Theorem ralimdv2 3176

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  ralimdva  3179  zorn2lem7  10501  pwfseqlem3  10660  sup2  12186  xrsupexmnf  13347  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  r19.29uz  15426  rexuzre  15428  caurcvg  15752  caucvg  15754  isprm5  16788  prmgaplem5  17137  prmgaplem6  17138  mrissmrid  17719  elcls3  23290  iscnp4  23470  cncls2  23480  cnntr  23482  2ndcsep  23667  dyadmbllem  25809  xrlimcnp  27184  pntlem3  27824  lfuhgr2  29554  fldextrspunlsplem  34127  sigaclfu2  34575  rdgssun  38081  mapdordlem2  42469  aks6d1c1  42941  sn-sup2  43323  dffltz  43424  cantnfresb  44109  safesnsupfiub  44200  iunrelexp0  44486  climrec  46377  0ellimcdiv  46421  pgindnf  50551