Theorem ralimdv2 3153

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

Syntax hints:   → wi 4  ∀wal 1532   ∈ wcel 2099  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-ral 3052

This theorem is referenced by:  ralimdva  3157  ssralvOLD  4052  zorn2lem7  10545  pwfseqlem3  10703  sup2  12222  xrsupexmnf  13338  xrinfmexpnf  13339  xrsupsslem  13340  xrinfmsslem  13341  xrub  13345  r19.29uz  15355  rexuzre  15357  caurcvg  15681  caucvg  15683  isprm5  16708  prmgaplem5  17057  prmgaplem6  17058  mrissmrid  17654  elcls3  23078  iscnp4  23258  cncls2  23268  cnntr  23270  2ndcsep  23454  dyadmbllem  25619  xrlimcnp  26996  pntlem3  27638  sigaclfu2  33954  lfuhgr2  34946  rdgssun  37085  mapdordlem2  41336  aks6d1c1  41814  sn-sup2  42251  dffltz  42288  cantnfresb  42990  safesnsupfiub  43083  iunrelexp0  43369  climrec  45224  0ellimcdiv  45270  pgindnf  48462