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

Theorem rexralbidv 3188
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 3116 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 3182 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 3042  wrex 3043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-ral 3047  df-rex 3048
This theorem is referenced by:  freq1  5228  rexfiuz  14278  cau3lem  14285  caubnd2  14288  climi  14432  rlimi  14435  o1lo1  14459  2clim  14494  lo1le  14573  caucvgrlem  14594  caurcvgr  14595  caucvgb  14601  vdwlem10  15888  vdwlem13  15891  pmatcollpw2lem  20776  neiptopnei  21130  lmcvg  21260  lmss  21296  elpt  21569  elptr  21570  txlm  21645  tsmsi  22130  ustuqtop4  22241  isucn  22275  isucn2  22276  ucnima  22278  metcnpi  22542  metcnpi2  22543  metucn  22569  xrge0tsms  22830  elcncf  22885  cncfi  22890  lmmcvg  23251  lhop1  23968  ulmval  24325  ulmi  24331  ulmcaulem  24339  ulmdvlem3  24347  pntibnd  25473  pntlem3  25489  pntleml  25491  axtgcont1  25558  perpln1  25796  perpln2  25797  isperp  25798  brbtwn  25970  uvtx01vtx  26492  isgrpo  27652  ubthlem3  28029  ubth  28030  hcau  28342  hcaucvg  28344  hlimi  28346  hlimconvi  28349  hlim2  28350  elcnop  29017  elcnfn  29042  cnopc  29073  cnfnc  29090  lnopcon  29195  lnfncon  29216  riesz1  29225  xrge0tsmsd  30086  signsply0  30929  limcleqr  40371  addlimc  40375  0ellimcdiv  40376  climd  40399  climisp  40473  lmbr3  40474  climrescn  40475  climxrrelem  40476  climxrre  40477  xlimxrre  40552  xlimmnf  40562  xlimpnf  40563  xlimmnfmpt  40564  xlimpnfmpt  40565  dfxlim2  40569  cncfshift  40582  cncfperiod  40587  ioodvbdlimc1lem1  40641  ioodvbdlimc1lem2  40642  ioodvbdlimc2lem  40644  fourierdlem68  40886  fourierdlem87  40905  fourierdlem103  40921  fourierdlem104  40922  etransclem48  40994
  Copyright terms: Public domain W3C validator