Theorem ralimdv2 3143

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3049

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

This theorem depends on definitions:  df-bi 207  df-ral 3050

This theorem is referenced by:  ralimdva  3146  ssralvOLD  4004  zorn2lem7  10410  pwfseqlem3  10569  sup2  12096  xrsupexmnf  13218  xrinfmexpnf  13219  xrsupsslem  13220  xrinfmsslem  13221  xrub  13225  r19.29uz  15272  rexuzre  15274  caurcvg  15598  caucvg  15600  isprm5  16632  prmgaplem5  16981  prmgaplem6  16982  mrissmrid  17562  elcls3  23025  iscnp4  23205  cncls2  23215  cnntr  23217  2ndcsep  23401  dyadmbllem  25554  xrlimcnp  26932  pntlem3  27574  fldextrspunlsplem  33779  sigaclfu2  34227  lfuhgr2  35262  rdgssun  37522  mapdordlem2  41836  aks6d1c1  42309  sn-sup2  42688  dffltz  42819  cantnfresb  43508  safesnsupfiub  43599  iunrelexp0  43885  climrec  45791  0ellimcdiv  45835  pgindnf  49903