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 1949	. 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 1568   ∈ wcel 2145  ∀wral 3076

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 3077

This theorem is used by:  ralimdva  3174  zorn2lem7  10504  pwfseqlem3  10669  sup2  12195  xrsupexmnf  13357  xrinfmexpnf  13358  xrsupsslem  13359  xrinfmsslem  13360  xrub  13364  r19.29uz  15438  rexuzre  15440  caurcvg  15764  caucvg  15766  isprm5  16798  prmgaplem5  17147  prmgaplem6  17148  mrissmrid  17729  elcls3  23308  iscnp4  23488  cncls2  23498  cnntr  23500  2ndcsep  23685  dyadmbllem  25827  xrlimcnp  27205  pntlem3  27845  lfuhgr2  29606  fldextrspunlsplem  34183  sigaclfu2  34631  rdgssun  38132  mapdordlem2  42510  aks6d1c1  42982  sn-sup2  43379  dffltz  43480  cantnfresb  44165  safesnsupfiub  44256  iunrelexp0  44542  climrec  46433  0ellimcdiv  46477  pgindnf  50642