Theorem rexbidva 2502

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2175  ∃wrex 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-rex 2489

This theorem is referenced by:  2rexbiia  2521  2rexbidva  2528  rexeqbidva  2720  dfimafn  5621  funimass4  5623  fconstfvm  5792  fliftel  5852  fliftf  5858  f1oiso  5885  releldm2  6261  frecabcl  6475  qsinxp  6688  qliftel  6692  supisolem  7092  enumctlemm  7198  ismkvnex  7239  genpassl  7619  genpassu  7620  addcomprg  7673  mulcomprg  7675  1idprl  7685  1idpru  7686  archrecnq  7758  archrecpr  7759  caucvgprprlemexbt  7801  caucvgprprlemexb  7802  archsr  7877  map2psrprg  7900  suplocsrlempr  7902  axsuploc  8127  cnegexlem3  8231  cnegex2  8233  recexre  8633  rerecclap  8785  creur  9014  creui  9015  nndiv  9059  arch  9274  nnrecl  9275  expnlbnd  10790  fimaxq  10953  wrdval  10972  clim2  11513  clim2c  11514  clim0c  11516  climabs0  11537  climrecvg1n  11578  sumeq2  11589  mertensabs  11767  prodeq2  11787  zproddc  11809  nndivides  12027  alzdvds  12084  oddm1even  12105  oddnn02np1  12110  oddge22np1  12111  evennn02n  12112  evennn2n  12113  divalgb  12155  modremain  12159  modprmn0modprm0  12498  pythagtriplem2  12508  pythagtrip  12525  pceu  12537  4sqlem12  12644  gsumpropd2  13143  mndpfo  13188  mndpropd  13190  grppropd  13267  conjnmzb  13534  dvdsr02  13785  crngunit  13791  dvdsrpropdg  13827  cnfldui  14269  znunit  14339  iscnp3  14593  lmbrf  14605  cncnp  14620  lmss  14636  metrest  14896  metcnp  14902  metcnp2  14903  txmetcnp  14908  cdivcncfap  14994  ivthdec  15034  lgsquadlem2  15473  2lgslem1a  15483  pw1nct  15804