Theorem 2rexbidv 2575

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
2rexbidv	|- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)   A( x, y)   B( x, y)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	rexbidv 2551	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2551	1 |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  f1oiso  6032  elrnmpog  6201  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovelrn  6238  eroveu  6900  genipv  7876  genpelxp  7878  genpelvl  7879  genpelvu  7880  axcnre  8248  apreap  8917  apreim  8933  aprcl  8976  aptap  8980  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  pythagtriplem19  13081  pceu  13094  pcval  13095  pczpre  13096  pcdiv  13101  4sqlem2  13188  4sqlem3  13189  4sqlem4  13191  4sqexercise2  13198  4sqlemsdc  13199  4sq  13209  znunit  15043  txuni2  15406  txbas  15408  txdis1cn  15428  elply  15884  2sqlem2  16332  2sqlem8  16340  2sqlem9  16341  upgredg  16483  3dom  17116