Theorem 2rexbidv 2531

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 2507	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2507	1 |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.wrex 2485

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-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  f1oiso  5895  elrnmpog  6058  elrnmpo  6059  ralrnmpo  6060  rexrnmpo  6061  ovelrn  6095  eroveu  6713  genipv  7622  genpelxp  7624  genpelvl  7625  genpelvu  7626  axcnre  7994  apreap  8660  apreim  8676  aprcl  8719  aptap  8723  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  pythagtriplem19  12605  pceu  12618  pcval  12619  pczpre  12620  pcdiv  12625  4sqlem2  12712  4sqlem3  12713  4sqlem4  12715  4sqexercise2  12722  4sqlemsdc  12723  4sq  12733  znunit  14421  txuni2  14728  txbas  14730  txdis1cn  14750  elply  15206  2sqlem2  15592  2sqlem8  15600  2sqlem9  15601