Theorem ralimdv2 3148

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

Step	Hyp	Ref	Expression
1		ralimdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒)))
2	1	alimdv 1923	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 3054	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3054	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3imtr4g 297	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  ralimdva  3151  zorn2lem7  10415  pwfseqlem3  10574  sup2  12103  xrsupexmnf  13248  xrinfmexpnf  13249  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  r19.29uz  15304  rexuzre  15306  caurcvg  15630  caucvg  15632  isprm5  16668  prmgaplem5  17017  prmgaplem6  17018  mrissmrid  17598  elcls3  23066  iscnp4  23246  cncls2  23256  cnntr  23258  2ndcsep  23442  dyadmbllem  25584  xrlimcnp  26950  pntlem3  27590  fldextrspunlsplem  33857  sigaclfu2  34305  lfuhgr2  35347  rdgssun  37740  mapdordlem2  42129  aks6d1c1  42601  sn-sup2  42981  dffltz  43084  cantnfresb  43769  safesnsupfiub  43860  iunrelexp0  44146  climrec  46048  0ellimcdiv  46092  pgindnf  50206