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  8503  cnegex2  8505  recexre  8906  rerecclap  9060  creur  9289  creui  9290  nndiv  9345  arch  9560  nnrecl  9561  expnlbnd  11102  fimaxq  11270  wrdval  11307  clim2  12049  clim2c  12050  clim0c  12052  climabs0  12073  climrecvg1n  12114  sumeq2  12125  mertensabs  12304  prodeq2  12324  zproddc  12346  nndivides  12564  alzdvds  12621  oddm1even  12642  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  divalgb  12692  modremain  12696  modprmn0modprm0  13035  pythagtriplem2  13045  pythagtrip  13062  pceu  13074  4sqlem12  13181  ballotfilemsima  13259  mndpfo  13751  mndpropd  13753  grppropd  13822  conjnmzb  14083  dvdsr02  14412  crngunit  14418  dvdsrpropdg  14454  cnfldui  14924  znunit  14994  iscnp3  15304  lmbrf  15316  cncnp  15331  lmss  15347  metrest  15607  metcnp  15613  metcnp2  15614  txmetcnp  15619  cdivcncfap  15705  ivthdec  15745  lgsquadlem2  16197  2lgslem1a  16207  pw1nct  17033