Theorem r19.21aivv 1727

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

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

This theorem is referenced by:  r19.21advv 1728  wereu 2959  ralxp 3232  dom2d 4418  fiint 4570  rankxplim 4724  lbreu 6051  uzwo5OLD 6220  acdc3lem 7501  acdc2lem2 7504  acdc5lem2 7507  acdclem 7509  acdcALT 7511  tgclt 7636  topbast 7639  blrn 7850  blf 7853  opntop 7879  tgbl 7880  blbas 7881  xpcn 7985  grpinvf 8087  grpdivf 8093  grplactf1o 8106  subgabl 8131  ghgrpi 8145  nvmf 8274  va1cnlem 8353  ipf 8374  sspg 8395  ssps 8397  sspmlem 8399  0lno 8458  sspph 8523  ipblnfi 8524  unopf1ot 9847  cnvunopt 9849  unoplint 9851  counopt 9852  adjadjt 9867  unopadj2t 9869  hmopadjt 9870  hmopadj2t 9872  hmoplint 9873  bralnfnt 9879  lnopm 9932  lnopeq0 9939  hmopst 9952  hmopmt 9953  hmopcot 9955  lnopcon 9970  lnfncon 9997  cnlnadjlem2 10008  adjlnopt 10026  adjmult 10032  adjaddt 10033  cdjreu 10367  ghomf1olem 10404  hmeogrp 10544  homcard 10545  neifil 10573  filintf 10574  rcfpfillem4 10586  trnij 10628  idmon 10736  idfisf 10752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 967  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982

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

Copyright terms: Public domain