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  6035  elrnmpog  6204  elrnmpo  6205  ralrnmpo  6206  rexrnmpo  6207  ovelrn  6241  eroveu  6904  genipv  7882  genpelxp  7884  genpelvl  7885  genpelvu  7886  axcnre  8254  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  pythagtriplem19  13090  pceu  13103  pcval  13104  pczpre  13105  pcdiv  13110  4sqlem2  13197  4sqlem3  13198  4sqlem4  13200  4sqexercise2  13207  4sqlemsdc  13208  4sq  13218  znunit  15103  txuni2  15482  txbas  15484  txdis1cn  15504  elply  15960  2sqlem2  16439  2sqlem8  16447  2sqlem9  16448  upgredg  16590  3dom  17223