Theorem ralimdv2 3171

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  ralimdva  3174  tz7.48lem  8457  zorn2lem7  10587  pwfseqlem3  10752  sup2  12280  xrsupexmnf  13442  xrinfmexpnf  13443  xrsupsslem  13444  xrinfmsslem  13445  xrub  13449  r19.29uz  15527  rexuzre  15529  caurcvg  15853  caucvg  15855  isprm5  16892  prmgaplem5  17242  prmgaplem6  17243  mrissmrid  17824  elcls3  23410  iscnp4  23590  cncls2  23600  cnntr  23602  2ndcsep  23787  dyadmbllem  25929  xrlimcnp  27305  pntlem3  27945  lfuhgr2  29736  fldextrspunlsplem  34355  sigaclfu2  34803  rdgssun  38410  mapdordlem2  42803  aks6d1c1  43275  sn-sup2  43664  dffltz  43779  cantnfresb  44435  safesnsupfiub  44526  iunrelexp0  44811  climrec  46723  0ellimcdiv  46767  pgindnf  50992