Theorem reubidv 2260

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

Hypothesis

Ref	Expression
reubidv.1	|- (ph -> (ps <-> ch))

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		reubidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	adantr 425	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	2	reubidva 2259	1 |- (ph -> (E!x e. A ps <-> E!x e. A ch))

Syntax hints:   -> wi 3   <-> wb 163   e. wcel 1300  E!wreu 2107

This theorem is referenced by:  reueqd 2273  eufromeq6 3833  oawordeu 5237  riotabidv 5562  aceq6b 5904  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  riesz4 11634  cnlnadjlem4 11640  cnlnadjeu 11648  bnj1319 13495  divalg 13706  divalg2 13708  efp2 15290  bfplem11 16008

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-eu 1775  df-reu 2111

Copyright terms: Public domain