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  5681  funimass4  5683  fconstfvm  5856  fliftel  5916  fliftf  5922  f1oiso  5949  releldm2  6329  frecabcl  6543  qsinxp  6756  qliftel  6760  supisolem  7171  enumctlemm  7277  ismkvnex  7318  genpassl  7707  genpassu  7708  addcomprg  7761  mulcomprg  7763  1idprl  7773  1idpru  7774  archrecnq  7846  archrecpr  7847  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  archsr  7965  map2psrprg  7988  suplocsrlempr  7990  axsuploc  8215  cnegexlem3  8319  cnegex2  8321  recexre  8721  rerecclap  8873  creur  9102  creui  9103  nndiv  9147  arch  9362  nnrecl  9363  expnlbnd  10881  fimaxq  11044  wrdval  11069  clim2  11789  clim2c  11790  clim0c  11792  climabs0  11813  climrecvg1n  11854  sumeq2  11865  mertensabs  12043  prodeq2  12063  zproddc  12085  nndivides  12303  alzdvds  12360  oddm1even  12381  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  divalgb  12431  modremain  12435  modprmn0modprm0  12774  pythagtriplem2  12784  pythagtrip  12801  pceu  12813  4sqlem12  12920  gsumpropd2  13421  mndpfo  13466  mndpropd  13468  grppropd  13545  conjnmzb  13812  dvdsr02  14063  crngunit  14069  dvdsrpropdg  14105  cnfldui  14547  znunit  14617  iscnp3  14871  lmbrf  14883  cncnp  14898  lmss  14914  metrest  15174  metcnp  15180  metcnp2  15181  txmetcnp  15186  cdivcncfap  15272  ivthdec  15312  lgsquadlem2  15751  2lgslem1a  15761  pw1nct  16328