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  8915  apreim  8931  aprcl  8974  aptap  8978  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  pythagtriplem19  13061  pceu  13074  pcval  13075  pczpre  13076  pcdiv  13081  4sqlem2  13168  4sqlem3  13169  4sqlem4  13171  4sqexercise2  13178  4sqlemsdc  13179  4sq  13189  znunit  14994  txuni2  15357  txbas  15359  txdis1cn  15379  elply  15835  2sqlem2  16234  2sqlem8  16242  2sqlem9  16243  upgredg  16385  3dom  17018