Theorem rexbidva 2462

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 1516	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2460	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-rex 2449

This theorem is referenced by:  2rexbiia  2481  2rexbidva  2488  rexeqbidva  2675  dfimafn  5534  funimass4  5536  fconstfvm  5702  fliftel  5760  fliftf  5766  f1oiso  5793  releldm2  6150  frecabcl  6363  qsinxp  6573  qliftel  6577  supisolem  6969  enumctlemm  7075  ismkvnex  7115  genpassl  7461  genpassu  7462  addcomprg  7515  mulcomprg  7517  1idprl  7527  1idpru  7528  archrecnq  7600  archrecpr  7601  caucvgprprlemexbt  7643  caucvgprprlemexb  7644  archsr  7719  map2psrprg  7742  suplocsrlempr  7744  axsuploc  7967  cnegexlem3  8071  cnegex2  8073  recexre  8472  rerecclap  8622  creur  8850  creui  8851  nndiv  8894  arch  9107  nnrecl  9108  expnlbnd  10575  fimaxq  10736  clim2  11220  clim2c  11221  clim0c  11223  climabs0  11244  climrecvg1n  11285  sumeq2  11296  mertensabs  11474  prodeq2  11494  zproddc  11516  nndivides  11733  alzdvds  11788  oddm1even  11808  oddnn02np1  11813  oddge22np1  11814  evennn02n  11815  evennn2n  11816  divalgb  11858  modremain  11862  modprmn0modprm0  12184  pythagtriplem2  12194  pythagtrip  12211  pceu  12223  iscnp3  12803  lmbrf  12815  cncnp  12830  lmss  12846  metrest  13106  metcnp  13112  metcnp2  13113  txmetcnp  13118  cdivcncfap  13187  ivthdec  13222  pw1nct  13843