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

Theorem rexralbidv 3246
Description: Formula-building rule for restricted quantifiers (deduction form). (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 3147 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 3242 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wral 3088  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3093  df-rex 3094
This theorem is referenced by:  freq1  5377  rexfiuz  14568  cau3lem  14575  caubnd2  14578  climi  14728  rlimi  14731  o1lo1  14755  2clim  14790  lo1le  14869  caucvgrlem  14890  caurcvgr  14891  caucvgb  14897  vdwlem10  16182  vdwlem13  16185  pmatcollpw2lem  21089  neiptopnei  21444  lmcvg  21574  lmss  21610  elpt  21884  elptr  21885  txlm  21960  tsmsi  22445  ustuqtop4  22556  isucn  22590  isucn2  22591  ucnima  22593  metcnpi  22857  metcnpi2  22858  metucn  22884  xrge0tsms  23145  elcncf  23200  cncfi  23205  lmmcvg  23567  lhop1  24314  ulmval  24671  ulmi  24677  ulmcaulem  24685  ulmdvlem3  24693  pntibnd  25871  pntlem3  25887  pntleml  25889  axtgcont1  25956  perpln1  26198  perpln2  26199  isperp  26200  brbtwn  26388  uvtx01vtx  26882  isgrpo  28051  ubthlem3  28427  ubth  28428  hcau  28740  hcaucvg  28742  hlimi  28744  hlimconvi  28747  hlim2  28748  elcnop  29415  elcnfn  29440  cnopc  29471  cnfnc  29488  lnopcon  29593  lnfncon  29614  riesz1  29623  xrge0tsmsd  30536  signsply0  31473  unblimceq0  33372  limcleqr  41362  addlimc  41366  0ellimcdiv  41367  climd  41390  climisp  41464  lmbr3  41465  climrescn  41466  climxrrelem  41467  climxrre  41468  xlimpnfxnegmnf  41532  xlimxrre  41549  xlimmnf  41559  xlimpnf  41560  xlimmnfmpt  41561  xlimpnfmpt  41562  dfxlim2  41566  cncfshift  41593  cncfperiod  41598  ioodvbdlimc1lem1  41652  ioodvbdlimc1lem2  41653  ioodvbdlimc2lem  41655  fourierdlem68  41896  fourierdlem87  41915  fourierdlem103  41931  fourierdlem104  41932  etransclem48  42004
  Copyright terms: Public domain W3C validator