Theorem rexbidv 2636

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 2634	1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2621

This theorem is referenced by:  rexbii  2640  2rexbidv  2658  rexralbidv  2659  rexeqbi1dv  2817  rexeqbidv  2821  cbvrex2v  2845  rspc2ev  2964  rspc3ev  2966  ceqsrex2v  2975  sbcrexg  3122  uniiunlem  3354  eliun  3974  dfiin2g  4001  pwadjoin  4120  xpkeq2  4200  imakeq1  4225  elimakg  4258  nnc0suc  4413  opklefing  4449  opkltfing  4450  leltfintr  4459  lefinlteq  4464  ncfinraise  4482  ncfinlower  4484  nnpw1ex  4485  tfinprop  4490  tfinltfinlem1  4501  0ceven  4506  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnadjoinpw  4522  nnpweq  4524  tfinnn  4535  vfinncvntsp  4550  vfinspsslem1  4551  vfinspss  4552  dfphi2  4570  phi11lem1  4596  0cnelphi  4598  proj1op  4601  proj2op  4602  phialllem1  4617  elima  4755  imaeq1  4938  funcnvuni  5162  fun11iun  5306  fvelrnb  5366  fvelimab  5371  fnasrn  5418  foelrn  5426  foco2  5427  abrexco  5464  funiunfv  5468  f1oiso  5500  f1oiso2  5501  clos1basesuc  5883  qseq2  5976  elqsg  5977  brlecg  6113  ovmuc  6131  ncspw1eu  6160  eqtc  6162  lec0cg  6199  sbth  6207  dflec2  6211  letc  6232  ce0t  6233  ce0lenc1  6240  tcfnex  6245  nncdiv3  6278