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

Theorem ralimdv2 3153
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
Hypothesis
Ref Expression
ralimdv2.1 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
Assertion
Ref Expression
ralimdv2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem ralimdv2
StepHypRef Expression
1 ralimdv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
21alimdv 1912 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3052 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3052 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 295 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1532  wcel 2099  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-ral 3052
This theorem is referenced by:  ralimdva  3157  ssralvOLD  4052  zorn2lem7  10545  pwfseqlem3  10703  sup2  12222  xrsupexmnf  13338  xrinfmexpnf  13339  xrsupsslem  13340  xrinfmsslem  13341  xrub  13345  r19.29uz  15355  rexuzre  15357  caurcvg  15681  caucvg  15683  isprm5  16708  prmgaplem5  17057  prmgaplem6  17058  mrissmrid  17654  elcls3  23078  iscnp4  23258  cncls2  23268  cnntr  23270  2ndcsep  23454  dyadmbllem  25619  xrlimcnp  26996  pntlem3  27638  sigaclfu2  33954  lfuhgr2  34946  rdgssun  37085  mapdordlem2  41336  aks6d1c1  41814  sn-sup2  42251  dffltz  42288  cantnfresb  42990  safesnsupfiub  43083  iunrelexp0  43369  climrec  45224  0ellimcdiv  45270  pgindnf  48462
  Copyright terms: Public domain W3C validator