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

Theorem rexbidva 2502
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 1550 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2rexbida 2500 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wcel 2175  wrex 2484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556
This theorem depends on definitions:  df-bi 117  df-nf 1483  df-rex 2489
This theorem is referenced by:  2rexbiia  2521  2rexbidva  2528  rexeqbidva  2720  dfimafn  5621  funimass4  5623  fconstfvm  5792  fliftel  5852  fliftf  5858  f1oiso  5885  releldm2  6261  frecabcl  6475  qsinxp  6688  qliftel  6692  supisolem  7092  enumctlemm  7198  ismkvnex  7239  genpassl  7619  genpassu  7620  addcomprg  7673  mulcomprg  7675  1idprl  7685  1idpru  7686  archrecnq  7758  archrecpr  7759  caucvgprprlemexbt  7801  caucvgprprlemexb  7802  archsr  7877  map2psrprg  7900  suplocsrlempr  7902  axsuploc  8127  cnegexlem3  8231  cnegex2  8233  recexre  8633  rerecclap  8785  creur  9014  creui  9015  nndiv  9059  arch  9274  nnrecl  9275  expnlbnd  10790  fimaxq  10953  wrdval  10972  clim2  11513  clim2c  11514  clim0c  11516  climabs0  11537  climrecvg1n  11578  sumeq2  11589  mertensabs  11767  prodeq2  11787  zproddc  11809  nndivides  12027  alzdvds  12084  oddm1even  12105  oddnn02np1  12110  oddge22np1  12111  evennn02n  12112  evennn2n  12113  divalgb  12155  modremain  12159  modprmn0modprm0  12498  pythagtriplem2  12508  pythagtrip  12525  pceu  12537  4sqlem12  12644  gsumpropd2  13143  mndpfo  13188  mndpropd  13190  grppropd  13267  conjnmzb  13534  dvdsr02  13785  crngunit  13791  dvdsrpropdg  13827  cnfldui  14269  znunit  14339  iscnp3  14593  lmbrf  14605  cncnp  14620  lmss  14636  metrest  14896  metcnp  14902  metcnp2  14903  txmetcnp  14908  cdivcncfap  14994  ivthdec  15034  lgsquadlem2  15473  2lgslem1a  15483  pw1nct  15804
  Copyright terms: Public domain W3C validator