Theorem rexbidv 2635

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
rexbidv	⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Distinct variable group:   φ,x

Allowed substitution hints:   ψ(x)   χ(x)   A(x)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxφ
2		ralbidv.1	. 2 ⊢ (φ → (ψ ↔ χ))
3	1, 2	rexbid 2633	1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Syntax hints:   → wi 4   ↔ wb 176  ∃wrex 2615

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-rex 2620

This theorem is referenced by:  rexbii  2639  2rexbidv  2657  rexralbidv  2658  rexeqbi1dv  2816  rexeqbidv  2820  cbvrex2v  2844  rspc2ev  2963  rspc3ev  2965  ceqsrex2v  2974  sbcrexg  3121  uniiunlem  3353  eliun  3973  dfiin2g  4000  pwadjoin  4119  xpkeq2  4199  imakeq1  4224  elimakg  4257  nnc0suc  4412  opklefing  4448  opkltfing  4449  leltfintr  4458  lefinlteq  4463  ncfinraise  4481  ncfinlower  4483  nnpw1ex  4484  tfinprop  4489  tfinltfinlem1  4500  0ceven  4505  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnadjoinpw  4521  nnpweq  4523  tfinnn  4534  vfinncvntsp  4549  vfinspsslem1  4550  vfinspss  4551  dfphi2  4569  phi11lem1  4595  0cnelphi  4597  proj1op  4600  proj2op  4601  phialllem1  4616  elima  4754  imaeq1  4937  funcnvuni  5161  fun11iun  5305  fvelrnb  5365  fvelimab  5370  fnasrn  5417  foelrn  5425  foco2  5426  abrexco  5463  funiunfv  5467  f1oiso  5499  f1oiso2  5500  clos1basesuc  5882  qseq2  5975  elqsg  5976  brlecg  6112  ovmuc  6130  ncspw1eu  6159  eqtc  6161  lec0cg  6198  sbth  6206  dflec2  6210  letc  6231  ce0t  6232  ce0lenc1  6239  tcfnex  6244  nncdiv3  6277