Theorem rexbidva 2474

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbiia  2493  2rexbidva  2500  rexeqbidva  2687  dfimafn  5564  funimass4  5566  fconstfvm  5734  fliftel  5793  fliftf  5799  f1oiso  5826  releldm2  6185  frecabcl  6399  qsinxp  6610  qliftel  6614  supisolem  7006  enumctlemm  7112  ismkvnex  7152  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  1idprl  7588  1idpru  7589  archrecnq  7661  archrecpr  7662  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  archsr  7780  map2psrprg  7803  suplocsrlempr  7805  axsuploc  8029  cnegexlem3  8133  cnegex2  8135  recexre  8534  rerecclap  8686  creur  8915  creui  8916  nndiv  8959  arch  9172  nnrecl  9173  expnlbnd  10644  fimaxq  10806  clim2  11290  clim2c  11291  clim0c  11293  climabs0  11314  climrecvg1n  11355  sumeq2  11366  mertensabs  11544  prodeq2  11564  zproddc  11586  nndivides  11803  alzdvds  11859  oddm1even  11879  oddnn02np1  11884  oddge22np1  11885  evennn02n  11886  evennn2n  11887  divalgb  11929  modremain  11933  modprmn0modprm0  12255  pythagtriplem2  12265  pythagtrip  12282  pceu  12294  mndpfo  12838  mndpropd  12840  grppropd  12892  dvdsr02  13272  crngunit  13278  dvdsrpropdg  13314  iscnp3  13673  lmbrf  13685  cncnp  13700  lmss  13716  metrest  13976  metcnp  13982  metcnp2  13983  txmetcnp  13988  cdivcncfap  14057  ivthdec  14092  pw1nct  14722