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  6905  genipv  7882  genpelxp  7884  genpelvl  7885  genpelvu  7886  axcnre  8254  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  pythagtriplem19  13089  pceu  13102  pcval  13103  pczpre  13104  pcdiv  13109  4sqlem2  13196  4sqlem3  13197  4sqlem4  13199  4sqexercise2  13206  4sqlemsdc  13207  4sq  13217  znunit  15102  txuni2  15499  txbas  15501  txdis1cn  15521  elply  15977  2sqlem2  16456  2sqlem8  16464  2sqlem9  16465  upgredg  16607  3dom  17240