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

Theorem rexbidva 2409
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
StepHypRef Expression
1 nfv 1491 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2rexbida 2407 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wcel 1463  wrex 2392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-rex 2397
This theorem is referenced by:  2rexbiia  2426  2rexbidva  2433  rexeqbidva  2616  dfimafn  5436  funimass4  5438  fconstfvm  5604  fliftel  5660  fliftf  5666  f1oiso  5693  releldm2  6049  frecabcl  6262  qsinxp  6471  qliftel  6475  supisolem  6861  enumctlemm  6965  ismkvnex  6995  genpassl  7296  genpassu  7297  addcomprg  7350  mulcomprg  7352  1idprl  7362  1idpru  7363  archrecnq  7435  archrecpr  7436  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  archsr  7554  map2psrprg  7577  suplocsrlempr  7579  axsuploc  7801  cnegexlem3  7903  cnegex2  7905  recexre  8303  rerecclap  8453  creur  8677  creui  8678  nndiv  8721  arch  8928  nnrecl  8929  expnlbnd  10367  fimaxq  10524  clim2  11003  clim2c  11004  clim0c  11006  climabs0  11027  climrecvg1n  11068  sumeq2  11079  mertensabs  11257  nndivides  11407  alzdvds  11459  oddm1even  11479  oddnn02np1  11484  oddge22np1  11485  evennn02n  11486  evennn2n  11487  divalgb  11529  modremain  11533  iscnp3  12278  lmbrf  12290  cncnp  12305  lmss  12321  metrest  12581  metcnp  12587  metcnp2  12588  txmetcnp  12593  cdivcncfap  12662  ivthdec  12697
  Copyright terms: Public domain W3C validator