Theorem r19.21aivv 1720

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)

Hypothesis

Ref	Expression
r19.21aivv.1	|- (ph -> ((x e. A /\ y e. B) -> ps))

Assertion

Ref	Expression
r19.21aivv	|- (ph -> A.x e. A A.y e. B ps)

Distinct variable groups:   x,y,ph   y,A

Proof of Theorem r19.21aivv

Step	Hyp	Ref	Expression
1		r19.21aivv.1	. . . 4 |- (ph -> ((x e. A /\ y e. B) -> ps))
2	1	exp3a 375	. . 3 |- (ph -> (x e. A -> (y e. B -> ps)))
3	2	r19.21adv 1718	. 2 |- (ph -> (x e. A -> A.y e. B ps))
4	3	r19.21aiv 1713	1 |- (ph -> A.x e. A A.y e. B ps)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  A.wral 1645

This theorem is referenced by:  r19.21advv 1721  wereu 2945  ralxp 3218  dom2d 4404  fiint 4559  fiintOLD 4560  rankxplim 4712  lbreu 6045  uzwo5OLD 6211  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  acdcALT 7496  tgclt 7624  topbast 7627  blrn 7841  blf 7844  opntop 7870  tgbl 7871  blbas 7872  xpcn 7976  grpinvf 8079  grpdivf 8085  grplactf1o 8098  subgabl 8123  ghgrpi 8137  nvmf 8266  va1cnlem 8345  ipf 8366  sspg 8387  ssps 8389  sspmlem 8391  0lno 8450  sspph 8515  ipblnfi 8516  unopf1ot 9840  cnvunopt 9842  unoplint 9844  counopt 9845  adjadjt 9860  unopadj2t 9862  hmopadjt 9863  hmopadj2t 9865  hmoplint 9866  bralnfnt 9872  lnopm 9925  lnopeq0 9932  hmopst 9945  hmopmt 9946  hmopcot 9948  lnopcon 9963  lnfncon 9990  cnlnadjlem2 10001  adjlnopt 10019  adjmult 10025  adjaddt 10026  cdjreu 10359  ghomf1olem 10396  hmeogrp 10538  homcard 10539  neifil 10568  filintf 10569  rcfpfillem4 10591  rcfpfillem4OLD 10592  trnij 10637  idmon 10745  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1649

Copyright terms: Public domain