Theorem 2rexbidv 2495

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 2471	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2471	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 104   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-rex 2454

This theorem is referenced by:  f1oiso  5803  elrnmpog  5963  elrnmpo  5964  ralrnmpo  5965  rexrnmpo  5966  ovelrn  5999  eroveu  6601  genipv  7460  genpelxp  7462  genpelvl  7463  genpelvu  7464  axcnre  7832  apreap  8495  apreim  8511  aprcl  8554  bezoutlemnewy  11940  bezoutlema  11943  bezoutlemb  11944  pythagtriplem19  12225  pceu  12238  pcval  12239  pczpre  12240  pcdiv  12245  4sqlem2  12330  4sqlem3  12331  4sqlem4  12333  txuni2  13011  txbas  13013  txdis1cn  13033  2sqlem2  13706  2sqlem8  13714  2sqlem9  13715