Theorem ralimdv2 3157

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 1917	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3imtr4g 296	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2104  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralimdva  3161  ssralv  3992  zorn2lem7  10304  pwfseqlem3  10462  sup2  11977  xrsupexmnf  13085  xrinfmexpnf  13086  xrsupsslem  13087  xrinfmsslem  13088  xrub  13092  r19.29uz  15107  rexuzre  15109  caurcvg  15433  caucvg  15435  isprm5  16457  prmgaplem5  16801  prmgaplem6  16802  mrissmrid  17395  elcls3  22279  iscnp4  22459  cncls2  22469  cnntr  22471  2ndcsep  22655  dyadmbllem  24808  xrlimcnp  26163  pntlem3  26802  sigaclfu2  32134  lfuhgr2  33125  rdgssun  35593  mapdordlem2  39693  sn-sup2  40476  dffltz  40508  iunrelexp0  41348  climrec  43193  0ellimcdiv  43239