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

Theorem rexralbidv 3053
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 2982 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 3047 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2908  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914
This theorem is referenced by:  freq1  5054  rexfiuz  14037  cau3lem  14044  caubnd2  14047  climi  14191  rlimi  14194  o1lo1  14218  2clim  14253  lo1le  14332  caucvgrlem  14353  caurcvgr  14354  caucvgb  14360  vdwlem10  15637  vdwlem13  15640  pmatcollpw2lem  20522  neiptopnei  20876  lmcvg  21006  lmss  21042  elpt  21315  elptr  21316  txlm  21391  tsmsi  21877  ustuqtop4  21988  isucn  22022  isucn2  22023  ucnima  22025  metcnpi  22289  metcnpi2  22290  metucn  22316  xrge0tsms  22577  elcncf  22632  cncfi  22637  lmmcvg  22999  lhop1  23715  ulmval  24072  ulmi  24078  ulmcaulem  24086  ulmdvlem3  24094  pntibnd  25216  pntlem3  25232  pntleml  25234  axtgcont1  25301  perpln1  25539  perpln2  25540  isperp  25541  brbtwn  25713  isgrpo  27239  ubthlem3  27616  ubth  27617  hcau  27929  hcaucvg  27931  hlimi  27933  hlimconvi  27936  hlim2  27937  elcnop  28604  elcnfn  28629  cnopc  28660  cnfnc  28677  lnopcon  28782  lnfncon  28803  riesz1  28812  xrge0tsmsd  29612  signsply0  30450  limcleqr  39312  addlimc  39316  0ellimcdiv  39317  climd  39340  cncfshift  39422  cncfperiod  39427  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  fourierdlem68  39728  fourierdlem87  39747  fourierdlem103  39763  fourierdlem104  39764  etransclem48  39836
  Copyright terms: Public domain W3C validator