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  5626  funimass4  5628  fconstfvm  5801  fliftel  5861  fliftf  5867  f1oiso  5894  releldm2  6270  frecabcl  6484  qsinxp  6697  qliftel  6701  supisolem  7109  enumctlemm  7215  ismkvnex  7256  genpassl  7636  genpassu  7637  addcomprg  7690  mulcomprg  7692  1idprl  7702  1idpru  7703  archrecnq  7775  archrecpr  7776  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  archsr  7894  map2psrprg  7917  suplocsrlempr  7919  axsuploc  8144  cnegexlem3  8248  cnegex2  8250  recexre  8650  rerecclap  8802  creur  9031  creui  9032  nndiv  9076  arch  9291  nnrecl  9292  expnlbnd  10807  fimaxq  10970  wrdval  10995  clim2  11565  clim2c  11566  clim0c  11568  climabs0  11589  climrecvg1n  11630  sumeq2  11641  mertensabs  11819  prodeq2  11839  zproddc  11861  nndivides  12079  alzdvds  12136  oddm1even  12157  oddnn02np1  12162  oddge22np1  12163  evennn02n  12164  evennn2n  12165  divalgb  12207  modremain  12211  modprmn0modprm0  12550  pythagtriplem2  12560  pythagtrip  12577  pceu  12589  4sqlem12  12696  gsumpropd2  13196  mndpfo  13241  mndpropd  13243  grppropd  13320  conjnmzb  13587  dvdsr02  13838  crngunit  13844  dvdsrpropdg  13880  cnfldui  14322  znunit  14392  iscnp3  14646  lmbrf  14658  cncnp  14673  lmss  14689  metrest  14949  metcnp  14955  metcnp2  14956  txmetcnp  14961  cdivcncfap  15047  ivthdec  15087  lgsquadlem2  15526  2lgslem1a  15536  pw1nct  15902