MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexralbidv Structured version   Visualization version   GIF version

Theorem rexralbidv 3036
Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2rexbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rexralbidv (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rexralbidv
StepHypRef Expression
1 2rexbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21ralbidv 2965 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 3030 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wral 2892  wrex 2893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2897  df-rex 2898
This theorem is referenced by:  freq1  4995  rexfiuz  13878  cau3lem  13885  caubnd2  13888  climi  14032  rlimi  14035  o1lo1  14059  2clim  14094  lo1le  14173  caucvgrlem  14194  caurcvgr  14195  caucvgb  14201  vdwlem10  15475  vdwlem13  15478  pmatcollpw2lem  20340  neiptopnei  20685  lmcvg  20815  lmss  20851  elpt  21124  elptr  21125  txlm  21200  tsmsi  21686  ustuqtop4  21797  isucn  21831  isucn2  21832  ucnima  21834  metcnpi  22097  metcnpi2  22098  metucn  22124  xrge0tsms  22374  elcncf  22428  cncfi  22433  lmmcvg  22782  lhop1  23495  ulmval  23852  ulmi  23858  ulmcaulem  23866  ulmdvlem3  23874  pntibnd  24996  pntlem3  25012  pntleml  25014  axtgcont1  25081  perpln1  25320  perpln2  25321  isperp  25322  brbtwn  25494  isgrpo  26498  ubthlem3  26915  ubth  26916  hcau  27228  hcaucvg  27230  hlimi  27232  hlimconvi  27235  hlim2  27236  elcnop  27903  elcnfn  27928  cnopc  27959  cnfnc  27976  lnopcon  28081  lnfncon  28102  riesz1  28111  xrge0tsmsd  28919  signsply0  29757  limcleqr  38512  addlimc  38516  0ellimcdiv  38517  climd  38540  cncfshift  38560  cncfperiod  38565  ioodvbdlimc1lem1  38622  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  fourierdlem68  38868  fourierdlem87  38887  fourierdlem103  38903  fourierdlem104  38904  etransclem48  38976
  Copyright terms: Public domain W3C validator