Theorem 2rexbidv 2558

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2517

This theorem is referenced by:  f1oiso  5977  elrnmpog  6144  elrnmpo  6145  ralrnmpo  6146  rexrnmpo  6147  ovelrn  6181  eroveu  6838  genipv  7789  genpelxp  7791  genpelvl  7792  genpelvu  7793  axcnre  8161  apreap  8826  apreim  8842  aprcl  8885  aptap  8889  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  pythagtriplem19  12935  pceu  12948  pcval  12949  pczpre  12950  pcdiv  12955  4sqlem2  13042  4sqlem3  13043  4sqlem4  13045  4sqexercise2  13052  4sqlemsdc  13053  4sq  13063  znunit  14755  txuni2  15067  txbas  15069  txdis1cn  15089  elply  15545  2sqlem2  15934  2sqlem8  15942  2sqlem9  15943  upgredg  16085  3dom  16708