Theorem birexdva 1216

Description: Formula-building rule for restricted existential quantifier (deduction rule).

Hypothesis

Ref	Expression
biraldva.1	|- ((ph /\ x e. A) -> (ps <-> ch))

Assertion

Ref	Expression
birexdva	|- (ph -> (E.x e. A ps <-> E.x e. A ch))

Distinct variable group(s):   ph,x

Proof of Theorem birexdva

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		biraldva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	birexda 1214	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   e. wcel 1092  E.wrex 1202

This theorem is referenced by:  bi2rexa 1230  bi2rexdva 1234  weinxp 2467  fconstfv 2903  isomin 2937  f1oiso 2942  oaass 3163  r1pwcl 3530  sup3 4511  nnreclt 4522  projlem1 5193  projlem2 5194  projlem26 5218  chrelat 5757

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-rex 1206

metamath.org