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

Theorem rexbidva 2474
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 1528 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2rexbida 2472 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wcel 2148  wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461
This theorem is referenced by:  2rexbiia  2493  2rexbidva  2500  rexeqbidva  2687  dfimafn  5564  funimass4  5566  fconstfvm  5734  fliftel  5793  fliftf  5799  f1oiso  5826  releldm2  6185  frecabcl  6399  qsinxp  6610  qliftel  6614  supisolem  7006  enumctlemm  7112  ismkvnex  7152  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  1idprl  7588  1idpru  7589  archrecnq  7661  archrecpr  7662  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  archsr  7780  map2psrprg  7803  suplocsrlempr  7805  axsuploc  8028  cnegexlem3  8132  cnegex2  8134  recexre  8533  rerecclap  8685  creur  8914  creui  8915  nndiv  8958  arch  9171  nnrecl  9172  expnlbnd  10641  fimaxq  10802  clim2  11286  clim2c  11287  clim0c  11289  climabs0  11310  climrecvg1n  11351  sumeq2  11362  mertensabs  11540  prodeq2  11560  zproddc  11582  nndivides  11799  alzdvds  11854  oddm1even  11874  oddnn02np1  11879  oddge22np1  11880  evennn02n  11881  evennn2n  11882  divalgb  11924  modremain  11928  modprmn0modprm0  12250  pythagtriplem2  12260  pythagtrip  12277  pceu  12289  mndpfo  12833  mndpropd  12835  grppropd  12887  dvdsr02  13267  crngunit  13273  dvdsrpropdg  13309  iscnp3  13634  lmbrf  13646  cncnp  13661  lmss  13677  metrest  13937  metcnp  13943  metcnp2  13944  txmetcnp  13949  cdivcncfap  14018  ivthdec  14053  pw1nct  14672
  Copyright terms: Public domain W3C validator