Theorem ralimdv2 3175

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

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

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 1945

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

This theorem is used by:  ralimdva  3178  tz7.48lem  8488  zorn2lem7  10619  pwfseqlem3  10784  sup2  12313  xrsupexmnf  13475  xrinfmexpnf  13476  xrsupsslem  13477  xrinfmsslem  13478  xrub  13482  r19.29uz  15562  rexuzre  15564  caurcvg  15888  caucvg  15890  isprm5  16927  prmgaplem5  17277  prmgaplem6  17278  mrissmrid  17865  elcls3  23456  iscnp4  23636  cncls2  23646  cnntr  23648  2ndcsep  23833  dyadmbllem  25975  xrlimcnp  27353  pntlem3  27993  lfuhgr2  29784  fldextrspunlsplem  34416  sigaclfu2  34864  rdgssun  38569  mapdordlem2  42960  aks6d1c1  43432  sn-sup2  43821  dffltz  43936  cantnfresb  44587  safesnsupfiub  44678  iunrelexp0  44963  climrec  46888  0ellimcdiv  46932  pgindnf  51215