ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexbidva GIF version

Theorem rexbidva 2371
Description: Formula-building rule for restricted existential quantifier (deduction rule). (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
StepHypRef Expression
1 nfv 1462 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2rexbida 2369 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wcel 1434  wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2359
This theorem is referenced by:  2rexbiia  2388  2rexbidva  2395  rexeqbidva  2570  dfimafn  5298  funimass4  5300  fconstfvm  5455  fliftel  5512  fliftf  5518  f1oiso  5544  releldm2  5890  frecabcl  6096  qsinxp  6298  qliftel  6302  supisolem  6610  genpassl  6986  genpassu  6987  addcomprg  7040  mulcomprg  7042  1idprl  7052  1idpru  7053  archrecnq  7125  archrecpr  7126  caucvgprprlemexbt  7168  caucvgprprlemexb  7169  archsr  7230  cnegexlem3  7562  cnegex2  7564  recexre  7955  rerecclap  8095  creur  8313  creui  8314  nndiv  8356  arch  8562  nnrecl  8563  expnlbnd  9913  clim2  10496  clim2c  10497  clim0c  10499  climabs0  10520  climrecvg1n  10559  sumeq2d  10570  sumeq2  10571  nndivides  10583  alzdvds  10635  oddm1even  10655  oddnn02np1  10660  oddge22np1  10661  evennn02n  10662  evennn2n  10663  divalgb  10705  modremain  10709
  Copyright terms: Public domain W3C validator