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  8450  zorn2lem7  10580  pwfseqlem3  10745  sup2  12273  xrsupexmnf  13435  xrinfmexpnf  13436  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  r19.29uz  15518  rexuzre  15520  caurcvg  15844  caucvg  15846  isprm5  16883  prmgaplem5  17233  prmgaplem6  17234  mrissmrid  17815  elcls3  23401  iscnp4  23581  cncls2  23591  cnntr  23593  2ndcsep  23778  dyadmbllem  25920  xrlimcnp  27296  pntlem3  27936  lfuhgr2  29727  fldextrspunlsplem  34305  sigaclfu2  34753  rdgssun  38302  mapdordlem2  42695  aks6d1c1  43167  sn-sup2  43556  dffltz  43671  cantnfresb  44326  safesnsupfiub  44417  iunrelexp0  44702  climrec  46615  0ellimcdiv  46659  pgindnf  50809