Theorem rexbidva 2529

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  2rexbiia  2548  2rexbidva  2555  rexeqbidva  2749  dfimafn  5694  funimass4  5696  fconstfvm  5871  fliftel  5933  fliftf  5939  f1oiso  5966  releldm2  6347  frecabcl  6564  qsinxp  6779  qliftel  6783  supisolem  7206  enumctlemm  7312  ismkvnex  7353  genpassl  7743  genpassu  7744  addcomprg  7797  mulcomprg  7799  1idprl  7809  1idpru  7810  archrecnq  7882  archrecpr  7883  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  archsr  8001  map2psrprg  8024  suplocsrlempr  8026  axsuploc  8251  cnegexlem3  8355  cnegex2  8357  recexre  8757  rerecclap  8909  creur  9138  creui  9139  nndiv  9183  arch  9398  nnrecl  9399  expnlbnd  10925  fimaxq  11090  wrdval  11115  clim2  11843  clim2c  11844  clim0c  11846  climabs0  11867  climrecvg1n  11908  sumeq2  11919  mertensabs  12097  prodeq2  12117  zproddc  12139  nndivides  12357  alzdvds  12414  oddm1even  12435  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  divalgb  12485  modremain  12489  modprmn0modprm0  12828  pythagtriplem2  12838  pythagtrip  12855  pceu  12867  4sqlem12  12974  gsumpropd2  13475  mndpfo  13520  mndpropd  13522  grppropd  13599  conjnmzb  13866  dvdsr02  14118  crngunit  14124  dvdsrpropdg  14160  cnfldui  14602  znunit  14672  iscnp3  14926  lmbrf  14938  cncnp  14953  lmss  14969  metrest  15229  metcnp  15235  metcnp2  15236  txmetcnp  15241  cdivcncfap  15327  ivthdec  15367  lgsquadlem2  15806  2lgslem1a  15816  pw1nct  16604