Theorem rexbidva 2547

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  2rexbiia  2566  2rexbidva  2573  rexeqbidva  2768  dfimafn  5751  funimass4  5753  fconstfvm  5933  dfimafnf  5955  fliftel  5999  fliftf  6005  f1oiso  6032  releldm2  6419  frecabcl  6670  qsinxp  6885  qliftel  6889  supisolem  7348  enumctlemm  7454  ismkvnex  7495  genpassl  7891  genpassu  7892  addcomprg  7945  mulcomprg  7947  1idprl  7957  1idpru  7958  archrecnq  8030  archrecpr  8031  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  archsr  8149  map2psrprg  8172  suplocsrlempr  8174  axsuploc  8398  cnegexlem3  8504  cnegex2  8506  recexre  8908  rerecclap  9062  creur  9291  creui  9292  nndiv  9347  arch  9564  nnrecl  9565  expnlbnd  11115  nn0sqdc  11160  fimaxq  11284  wrdval  11321  clim2  12065  clim2c  12066  clim0c  12068  climabs0  12089  climrecvg1n  12130  sumeq2  12141  mertensabs  12320  prodeq2  12340  zproddc  12362  nndivides  12580  alzdvds  12637  oddm1even  12658  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  divalgb  12708  modremain  12712  modprmn0modprm0  13055  pythagtriplem2  13065  pythagtrip  13082  pceu  13094  4sqlem12  13201  ballotfilemsima  13308  mndpfo  13800  mndpropd  13802  grppropd  13871  conjnmzb  14132  dvdsr02  14461  crngunit  14467  dvdsrpropdg  14503  cnfldui  14973  znunit  15043  iscnp3  15353  lmbrf  15365  cncnp  15380  lmss  15396  metrest  15656  metcnp  15662  metcnp2  15663  txmetcnp  15668  cdivcncfap  15754  ivthdec  15794  lgsquadlem2  16295  2lgslem1a  16305  pw1nct  17131