Theorem rexbidva 2435

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		nfv 1509	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2433	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1481  ∃wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2423

This theorem is referenced by:  2rexbiia  2454  2rexbidva  2461  rexeqbidva  2644  dfimafn  5478  funimass4  5480  fconstfvm  5646  fliftel  5702  fliftf  5708  f1oiso  5735  releldm2  6091  frecabcl  6304  qsinxp  6513  qliftel  6517  supisolem  6903  enumctlemm  7007  ismkvnex  7037  genpassl  7356  genpassu  7357  addcomprg  7410  mulcomprg  7412  1idprl  7422  1idpru  7423  archrecnq  7495  archrecpr  7496  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  archsr  7614  map2psrprg  7637  suplocsrlempr  7639  axsuploc  7861  cnegexlem3  7963  cnegex2  7965  recexre  8364  rerecclap  8514  creur  8741  creui  8742  nndiv  8785  arch  8998  nnrecl  8999  expnlbnd  10447  fimaxq  10605  clim2  11084  clim2c  11085  clim0c  11087  climabs0  11108  climrecvg1n  11149  sumeq2  11160  mertensabs  11338  prodeq2  11358  zproddc  11380  nndivides  11536  alzdvds  11588  oddm1even  11608  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  divalgb  11658  modremain  11662  iscnp3  12411  lmbrf  12423  cncnp  12438  lmss  12454  metrest  12714  metcnp  12720  metcnp2  12721  txmetcnp  12726  cdivcncfap  12795  ivthdec  12830  pw1nct  13371