Theorem rexbidva 2530

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 2528	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

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

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 2517

This theorem is referenced by:  2rexbiia  2549  2rexbidva  2556  rexeqbidva  2750  dfimafn  5703  funimass4  5705  fconstfvm  5880  fliftel  5944  fliftf  5950  f1oiso  5977  releldm2  6357  frecabcl  6608  qsinxp  6823  qliftel  6827  supisolem  7250  enumctlemm  7356  ismkvnex  7397  genpassl  7787  genpassu  7788  addcomprg  7841  mulcomprg  7843  1idprl  7853  1idpru  7854  archrecnq  7926  archrecpr  7927  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  archsr  8045  map2psrprg  8068  suplocsrlempr  8070  axsuploc  8294  cnegexlem3  8398  cnegex2  8400  recexre  8800  rerecclap  8952  creur  9181  creui  9182  nndiv  9226  arch  9441  nnrecl  9442  expnlbnd  10972  fimaxq  11137  wrdval  11165  clim2  11906  clim2c  11907  clim0c  11909  climabs0  11930  climrecvg1n  11971  sumeq2  11982  mertensabs  12161  prodeq2  12181  zproddc  12203  nndivides  12421  alzdvds  12478  oddm1even  12499  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  divalgb  12549  modremain  12553  modprmn0modprm0  12892  pythagtriplem2  12902  pythagtrip  12919  pceu  12931  4sqlem12  13038  gsumpropd2  13539  mndpfo  13584  mndpropd  13586  grppropd  13663  conjnmzb  13930  dvdsr02  14183  crngunit  14189  dvdsrpropdg  14225  cnfldui  14668  znunit  14738  iscnp3  14997  lmbrf  15009  cncnp  15024  lmss  15040  metrest  15300  metcnp  15306  metcnp2  15307  txmetcnp  15312  cdivcncfap  15398  ivthdec  15438  lgsquadlem2  15880  2lgslem1a  15890  pw1nct  16708