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  11536  clim2c  11537  clim0c  11539  climabs0  11560  climrecvg1n  11601  sumeq2  11612  mertensabs  11790  prodeq2  11810  zproddc  11832  nndivides  12050  alzdvds  12107  oddm1even  12128  oddnn02np1  12133  oddge22np1  12134  evennn02n  12135  evennn2n  12136  divalgb  12178  modremain  12182  modprmn0modprm0  12521  pythagtriplem2  12531  pythagtrip  12548  pceu  12560  4sqlem12  12667  gsumpropd2  13167  mndpfo  13212  mndpropd  13214  grppropd  13291  conjnmzb  13558  dvdsr02  13809  crngunit  13815  dvdsrpropdg  13851  cnfldui  14293  znunit  14363  iscnp3  14617  lmbrf  14629  cncnp  14644  lmss  14660  metrest  14920  metcnp  14926  metcnp2  14927  txmetcnp  14932  cdivcncfap  15018  ivthdec  15058  lgsquadlem2  15497  2lgslem1a  15507  pw1nct  15873