Theorem r19.21aivv 1723

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

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

This theorem is referenced by:  r19.21advv 1724  wereu 2951  ralxp 3224  dom2d 4410  fiint 4572  fiintOLD 4573  rankxplim 4722  lbreu 6047  uzwo5OLD 6213  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  acdclem 7495  acdcALT 7497  tgclt 7623  topbast 7626  blrn 7838  blf 7841  opntop 7867  tgbl 7868  blbas 7869  xpcn 7973  grpinvf 8075  grpdivf 8081  grplactf1o 8094  subgabl 8119  ghgrpi 8133  nvmf 8262  va1cnlem 8341  ipf 8362  sspg 8383  ssps 8385  sspmlem 8387  0lno 8446  sspph 8511  ipblnfi 8512  unopf1ot 9835  cnvunopt 9837  unoplint 9839  counopt 9840  adjadjt 9855  unopadj2t 9857  hmopadjt 9858  hmopadj2t 9860  hmoplint 9861  bralnfnt 9867  lnopm 9920  lnopeq0 9927  hmopst 9940  hmopmt 9941  hmopcot 9943  lnopcon 9958  lnfncon 9985  cnlnadjlem2 9996  adjlnopt 10014  adjmult 10020  adjaddt 10021  cdjreu 10354  ghomf1olem 10391  hmeogrp 10524  homcard 10525  neifil 10553  filintf 10554  rcfpfillem4 10566  trnij 10608  idmon 10716  idfisf 10731

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain