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

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

Proof of Theorem rexralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21ralbidv 3171 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 3172 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062  df-rex 3071
This theorem is referenced by:  freq1  5604  rexfiuz  15238  cau3lem  15245  caubnd2  15248  climi  15398  rlimi  15401  o1lo1  15425  2clim  15460  lo1le  15542  caucvgrlem  15563  caurcvgr  15564  caucvgb  15570  vdwlem10  16867  vdwlem13  16870  pmatcollpw2lem  22142  neiptopnei  22499  lmcvg  22629  lmss  22665  elpt  22939  elptr  22940  txlm  23015  tsmsi  23501  ustuqtop4  23612  isucn  23646  isucn2  23647  ucnima  23649  metcnpi  23916  metcnpi2  23917  metucn  23943  xrge0tsms  24213  elcncf  24268  cncfi  24273  lmmcvg  24641  lhop1  25394  ulmval  25755  ulmi  25761  ulmcaulem  25769  ulmdvlem3  25777  pntibnd  26957  pntlem3  26973  pntleml  26975  axtgcont1  27452  perpln1  27694  perpln2  27695  isperp  27696  brbtwn  27890  uvtx01vtx  28387  isgrpo  29481  ubthlem3  29856  ubth  29857  hcau  30168  hcaucvg  30170  hlimi  30172  hlimconvi  30175  hlim2  30176  elcnop  30841  elcnfn  30866  cnopc  30897  cnfnc  30914  lnopcon  31019  lnfncon  31040  riesz1  31049  xrge0tsmsd  31948  signsply0  33220  unblimceq0  35016  cvgcau  43812  limcleqr  43971  addlimc  43975  0ellimcdiv  43976  climd  43999  climisp  44073  lmbr3  44074  climrescn  44075  climxrrelem  44076  climxrre  44077  xlimpnfxnegmnf  44141  xlimxrre  44158  xlimmnf  44168  xlimpnf  44169  xlimmnfmpt  44170  xlimpnfmpt  44171  dfxlim2  44175  cncfshift  44201  cncfperiod  44206  ioodvbdlimc1lem1  44258  ioodvbdlimc1lem2  44259  ioodvbdlimc2lem  44261  fourierdlem68  44501  fourierdlem87  44520  fourierdlem103  44536  fourierdlem104  44537  etransclem48  44609
  Copyright terms: Public domain W3C validator