Theorem 2rexbidv 2414

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 2392	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2392	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 2371

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-rex 2376

This theorem is referenced by:  f1oiso  5643  elrnmpt2g  5795  elrnmpt2  5796  ralrnmpt2  5797  rexrnmpt2  5798  ovelrn  5831  eroveu  6423  genipv  7165  genpelxp  7167  genpelvl  7168  genpelvu  7169  axcnre  7513  apreap  8161  apreim  8177  bezoutlemnewy  11412  bezoutlema  11415  bezoutlemb  11416