Theorem ralxp 4875

Description: Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)

Hypothesis

Ref	Expression
ralxp.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )

Assertion

Ref	Expression
ralxp	|- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )

Distinct variable groups:   x, y, z, A   x, B, z   ph, y, z   ps, x   y, B

Allowed substitution hints:   ph( x)   ps( y, z)

Proof of Theorem ralxp

Step	Hyp	Ref	Expression
1		iunxpconst 4788	. . 3 |- U_ y e. A ( { y } X. B ) = ( A X. B )
2	1	raleqi 2733	. 2 |- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. x e. ( A X. B ) ph )
3		ralxp.1	. . 3 |- ( x = <. y , z >. -> ( ph <-> ps ) )
4	3	raliunxp 4873	. 2 |- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. y e. A A. z e. B ps )
5	2, 4	bitr3i 186	1 |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   A.wral 2509   {csn 3670   <.cop 3673   U_ciun 3971   X. cxp 4725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-sbc 3031  df-csb 3127  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-iun 3973  df-opab 4152  df-xp 4733  df-rel 4734

This theorem is referenced by:  ralxpf  4878  issref  5121  ffnov  6130  eqfnov  6133  funimassov  6177  f1stres  6327  f2ndres  6328  ecopover  6807  ecopoverg  6810  xpf1o  7035  imasaddfnlemg  13420  srgfcl  14010  txbas  15011  cnmpt21  15044  txmetcnp  15271  txmetcn  15272  qtopbasss  15274  mpodvdsmulf1o  15743  fsumdvdsmul  15744