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  5754  funimass4  5756  fconstfvm  5936  dfimafnf  5958  fliftel  6002  fliftf  6008  f1oiso  6035  releldm2  6423  frecabcl  6674  qsinxp  6889  qliftel  6893  supisolem  7354  enumctlemm  7460  ismkvnex  7501  genpassl  7897  genpassu  7898  addcomprg  7951  mulcomprg  7953  1idprl  7963  1idpru  7964  archrecnq  8036  archrecpr  8037  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  archsr  8155  map2psrprg  8178  suplocsrlempr  8180  axsuploc  8404  cnegexlem3  8510  cnegex2  8512  recexre  8914  rerecclap  9068  creur  9297  creui  9298  nndiv  9354  arch  9571  nnrecl  9572  expnlbnd  11123  nn0sqdc  11168  fimaxq  11292  wrdval  11329  clim2  12074  clim2c  12075  clim0c  12077  climabs0  12098  climrecvg1n  12139  sumeq2  12150  mertensabs  12329  prodeq2  12349  zproddc  12371  nndivides  12589  alzdvds  12646  oddm1even  12667  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  divalgb  12717  modremain  12721  modprmn0modprm0  13064  pythagtriplem2  13074  pythagtrip  13091  pceu  13103  4sqlem12  13210  ballotfilemsima  13317  mndpfo  13810  mndpropd  13812  grppropd  13881  conjnmzb  14142  dvdsr02  14521  crngunit  14527  dvdsrpropdg  14563  cnfldui  15033  znunit  15103  iscnp3  15429  lmbrf  15441  cncnp  15456  lmss  15472  metrest  15732  metcnp  15738  metcnp2  15739  txmetcnp  15744  cdivcncfap  15830  ivthdec  15870  bpos  16320  lgsquadlem2  16402  2lgslem1a  16412  pw1nct  17238