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  6675  qsinxp  6890  qliftel  6894  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  11122  nn0sqdc  11167  fimaxq  11291  wrdval  11328  clim2  12073  clim2c  12074  clim0c  12076  climabs0  12097  climrecvg1n  12138  sumeq2  12149  mertensabs  12328  prodeq2  12348  zproddc  12370  nndivides  12588  alzdvds  12645  oddm1even  12666  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  divalgb  12716  modremain  12720  modprmn0modprm0  13063  pythagtriplem2  13073  pythagtrip  13090  pceu  13102  4sqlem12  13209  ballotfilemsima  13316  mndpfo  13809  mndpropd  13811  grppropd  13880  conjnmzb  14141  dvdsr02  14520  crngunit  14526  dvdsrpropdg  14562  cnfldui  15032  znunit  15102  iscnp3  15446  lmbrf  15458  cncnp  15473  lmss  15489  metrest  15749  metcnp  15755  metcnp2  15756  txmetcnp  15761  cdivcncfap  15847  ivthdec  15887  bpos  16337  lgsquadlem2  16419  2lgslem1a  16429  pw1nct  17255