Theorem rexbidv 2369

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	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		nfv 1461	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	rexbid 2367	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 103  ∃wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-rex 2354

This theorem is referenced by:  rexbii  2373  2rexbidv  2391  rexralbidv  2392  rexeqbi1dv  2558  rexeqbidv  2562  cbvrex2v  2586  rspc2ev  2715  rspc3ev  2717  ceqsrex2v  2727  sbcrext  2891  uniiunlem  3082  eliun  3682  dfiin2g  3711  dfiunv2  3714  nn0suc  4345  rexxpf  4501  elrnmpt  4601  elrnmptg  4604  elimag  4692  funcnvuni  4988  fun11iun  5167  fvelrnb  5242  fvelimab  5250  foelrn  5338  foco2  5339  elabrex  5418  abrexco  5419  f1oiso  5485  f1oiso2  5486  acexmidlemab  5526  acexmidlemcase  5527  grprinvlem  5715  abrexex2g  5767  abrexex2  5771  recseq  5944  tfr0  5960  freceq1  6002  frec0g  6006  frecsuclem3  6013  frecsuc  6014  nnaordex  6123  qseq2  6178  elqsg  6179  isfi  6264  enfi  6358  supeq3  6403  supmoti  6406  suplubti  6413  supisolem  6421  cnvinfex  6431  eqinfti  6433  infvalti  6435  infglbti  6438  ltexnqq  6598  elinp  6664  prnmaxl  6678  prnminu  6679  prarloclem3  6687  ltdfpr  6696  genpdflem  6697  genipv  6699  genpassl  6714  genpassu  6715  ltexprlemm  6790  ltexprlemloc  6797  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlem2  6850  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemexbt  6896  caucvgprprlem2  6900  recexgt0sr  6950  archsr  6958  axprecex  7046  nntopi  7060  cnegex  7286  apreap  7687  recexap  7743  creur  8036  creui  8037  cju  8038  supinfneg  8683  infsupneg  8684  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  modqmuladd  9368  shftfvalg  9706  shftfval  9709  rexfiuz  9875  recvguniq  9881  fimaxre2  10109  clim  10120  sumeq1  10192  divides  10197  odd2np1lem  10271  opeo  10297  omeo  10298  divalglemeunn  10321  divalglemeuneg  10323  infssuzex  10345  zeqzmulgcd  10362  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemaz  10392  exprmfct  10519  bj-inf2vnlem1  10765  bj-inf2vnlem2  10766  bj-nn0sucALT  10773