Theorem rexbidva 2541

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2528

This theorem is referenced by:  2rexbiia  2560  2rexbidva  2567  rexeqbidva  2762  dfimafn  5730  funimass4  5732  fconstfvm  5907  dfimafnf  5928  fliftel  5972  fliftf  5978  f1oiso  6005  releldm2  6392  frecabcl  6643  qsinxp  6858  qliftel  6862  supisolem  7312  enumctlemm  7418  ismkvnex  7459  genpassl  7855  genpassu  7856  addcomprg  7909  mulcomprg  7911  1idprl  7921  1idpru  7922  archrecnq  7994  archrecpr  7995  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  archsr  8113  map2psrprg  8136  suplocsrlempr  8138  axsuploc  8362  cnegexlem3  8466  cnegex2  8468  recexre  8869  rerecclap  9021  creur  9250  creui  9251  nndiv  9295  arch  9510  nnrecl  9511  expnlbnd  11051  fimaxq  11219  wrdval  11252  clim2  11993  clim2c  11994  clim0c  11996  climabs0  12017  climrecvg1n  12058  sumeq2  12069  mertensabs  12248  prodeq2  12268  zproddc  12290  nndivides  12508  alzdvds  12565  oddm1even  12586  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  divalgb  12636  modremain  12640  modprmn0modprm0  12979  pythagtriplem2  12989  pythagtrip  13006  pceu  13018  4sqlem12  13125  ballotfilemsima  13203  gsumpropd2  13656  mndpfo  13699  mndpropd  13701  grppropd  13772  conjnmzb  14033  dvdsr02  14350  crngunit  14356  dvdsrpropdg  14392  cnfldui  14863  znunit  14933  iscnp3  15194  lmbrf  15206  cncnp  15221  lmss  15237  metrest  15497  metcnp  15503  metcnp2  15504  txmetcnp  15509  cdivcncfap  15595  ivthdec  15635  lgsquadlem2  16077  2lgslem1a  16087  pw1nct  16903