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  5690  funimass4  5692  fconstfvm  5867  fliftel  5929  fliftf  5935  f1oiso  5962  releldm2  6343  frecabcl  6560  qsinxp  6775  qliftel  6779  supisolem  7198  enumctlemm  7304  ismkvnex  7345  genpassl  7734  genpassu  7735  addcomprg  7788  mulcomprg  7790  1idprl  7800  1idpru  7801  archrecnq  7873  archrecpr  7874  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  archsr  7992  map2psrprg  8015  suplocsrlempr  8017  axsuploc  8242  cnegexlem3  8346  cnegex2  8348  recexre  8748  rerecclap  8900  creur  9129  creui  9130  nndiv  9174  arch  9389  nnrecl  9390  expnlbnd  10916  fimaxq  11081  wrdval  11106  clim2  11834  clim2c  11835  clim0c  11837  climabs0  11858  climrecvg1n  11899  sumeq2  11910  mertensabs  12088  prodeq2  12108  zproddc  12130  nndivides  12348  alzdvds  12405  oddm1even  12426  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  divalgb  12476  modremain  12480  modprmn0modprm0  12819  pythagtriplem2  12829  pythagtrip  12846  pceu  12858  4sqlem12  12965  gsumpropd2  13466  mndpfo  13511  mndpropd  13513  grppropd  13590  conjnmzb  13857  dvdsr02  14109  crngunit  14115  dvdsrpropdg  14151  cnfldui  14593  znunit  14663  iscnp3  14917  lmbrf  14929  cncnp  14944  lmss  14960  metrest  15220  metcnp  15226  metcnp2  15227  txmetcnp  15232  cdivcncfap  15318  ivthdec  15358  lgsquadlem2  15797  2lgslem1a  15807  pw1nct  16540