Theorem r19.21aivv 1717

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 1715	. 2 |- (ph -> (x e. A -> A.y e. B ps))
4	3	r19.21aiv 1710	1 |- (ph -> A.x e. A A.y e. B ps)

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

This theorem is referenced by:  r19.21advv 1718  wereu 2940  ralxp 3213  dom2d 4391  fiint 4540  rankxplim 4692  lbreu 6000  uzwo5OLD 6167  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  acdcALT 7446  tgclt 7574  topbast 7577  blrn 7793  blf 7796  opntop 7822  tgbl 7823  blbas 7824  xpcn 7926  grpinvf 8029  grpdivf 8035  grplactf1o 8049  subgabl 8075  ghgrpi 8089  nvmf 8218  va1cnlem 8292  ipf 8313  sspg 8334  ssps 8336  sspmlem 8338  0lno 8395  sspph 8459  ipblnfi 8460  unopf1ot 9779  cnvunopt 9781  unoplint 9783  counopt 9784  adjadjt 9799  unopadj2t 9801  hmopadjt 9802  hmopadj2t 9804  hmoplint 9805  bralnfnt 9811  lnopm 9863  lnopeq0 9870  hmopst 9883  hmopmt 9884  hmopcot 9886  lnopcon 9901  lnfncon 9928  cnlnadjlem2 9939  adjlnopt 9957  adjmult 9963  adjaddt 9964  cdjreu 10293  ghomf1olem 10330  hmeogrp 10461  homcard 10462  neifil 10478  filintf 10479  trnij 10517  idmon 10624

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain