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

Theorem rexbidva 2340
 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 1437 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2rexbida 2338 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∈ wcel 1409  ∃wrex 2324 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443 This theorem depends on definitions:  df-bi 114  df-nf 1366  df-rex 2329 This theorem is referenced by:  2rexbiia  2357  2rexbidva  2364  rexeqbidva  2537  dfimafn  5249  funimass4  5251  fconstfvm  5406  fliftel  5460  fliftf  5466  f1oiso  5492  releldm2  5838  qsinxp  6212  qliftel  6216  supisolem  6411  genpassl  6679  genpassu  6680  addcomprg  6733  mulcomprg  6735  1idprl  6745  1idpru  6746  archrecnq  6818  archrecpr  6819  caucvgprprlemexbt  6861  caucvgprprlemexb  6862  archsr  6923  cnegexlem3  7250  cnegex2  7252  recexre  7642  rerecclap  7780  creur  7986  creui  7987  nndiv  8029  arch  8235  nnrecl  8236  expnlbnd  9540  clim2  10034  clim2c  10035  clim0c  10037  climabs0  10058  climrecvg1n  10097  nndivides  10114  alzdvds  10165  oddm1even  10185  oddnn02np1  10191  oddge22np1  10192  evennn02n  10193  evennn2n  10194
 Copyright terms: Public domain W3C validator