Theorem rexbidva 2504

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2491

This theorem is referenced by:  2rexbiia  2523  2rexbidva  2530  rexeqbidva  2722  dfimafn  5640  funimass4  5642  fconstfvm  5815  fliftel  5875  fliftf  5881  f1oiso  5908  releldm2  6284  frecabcl  6498  qsinxp  6711  qliftel  6715  supisolem  7125  enumctlemm  7231  ismkvnex  7272  genpassl  7657  genpassu  7658  addcomprg  7711  mulcomprg  7713  1idprl  7723  1idpru  7724  archrecnq  7796  archrecpr  7797  caucvgprprlemexbt  7839  caucvgprprlemexb  7840  archsr  7915  map2psrprg  7938  suplocsrlempr  7940  axsuploc  8165  cnegexlem3  8269  cnegex2  8271  recexre  8671  rerecclap  8823  creur  9052  creui  9053  nndiv  9097  arch  9312  nnrecl  9313  expnlbnd  10831  fimaxq  10994  wrdval  11019  clim2  11669  clim2c  11670  clim0c  11672  climabs0  11693  climrecvg1n  11734  sumeq2  11745  mertensabs  11923  prodeq2  11943  zproddc  11965  nndivides  12183  alzdvds  12240  oddm1even  12261  oddnn02np1  12266  oddge22np1  12267  evennn02n  12268  evennn2n  12269  divalgb  12311  modremain  12315  modprmn0modprm0  12654  pythagtriplem2  12664  pythagtrip  12681  pceu  12693  4sqlem12  12800  gsumpropd2  13300  mndpfo  13345  mndpropd  13347  grppropd  13424  conjnmzb  13691  dvdsr02  13942  crngunit  13948  dvdsrpropdg  13984  cnfldui  14426  znunit  14496  iscnp3  14750  lmbrf  14762  cncnp  14777  lmss  14793  metrest  15053  metcnp  15059  metcnp2  15060  txmetcnp  15065  cdivcncfap  15151  ivthdec  15191  lgsquadlem2  15630  2lgslem1a  15640  pw1nct  16081