Theorem rexbidva 2527

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  2rexbiia  2546  2rexbidva  2553  rexeqbidva  2747  dfimafn  5684  funimass4  5686  fconstfvm  5861  fliftel  5923  fliftf  5929  f1oiso  5956  releldm2  6337  frecabcl  6551  qsinxp  6766  qliftel  6770  supisolem  7186  enumctlemm  7292  ismkvnex  7333  genpassl  7722  genpassu  7723  addcomprg  7776  mulcomprg  7778  1idprl  7788  1idpru  7789  archrecnq  7861  archrecpr  7862  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  archsr  7980  map2psrprg  8003  suplocsrlempr  8005  axsuploc  8230  cnegexlem3  8334  cnegex2  8336  recexre  8736  rerecclap  8888  creur  9117  creui  9118  nndiv  9162  arch  9377  nnrecl  9378  expnlbnd  10898  fimaxq  11062  wrdval  11087  clim2  11809  clim2c  11810  clim0c  11812  climabs0  11833  climrecvg1n  11874  sumeq2  11885  mertensabs  12063  prodeq2  12083  zproddc  12105  nndivides  12323  alzdvds  12380  oddm1even  12401  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  divalgb  12451  modremain  12455  modprmn0modprm0  12794  pythagtriplem2  12804  pythagtrip  12821  pceu  12833  4sqlem12  12940  gsumpropd2  13441  mndpfo  13486  mndpropd  13488  grppropd  13565  conjnmzb  13832  dvdsr02  14084  crngunit  14090  dvdsrpropdg  14126  cnfldui  14568  znunit  14638  iscnp3  14892  lmbrf  14904  cncnp  14919  lmss  14935  metrest  15195  metcnp  15201  metcnp2  15202  txmetcnp  15207  cdivcncfap  15293  ivthdec  15333  lgsquadlem2  15772  2lgslem1a  15782  pw1nct  16428