Theorem ralimdv2 3145

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

Syntax hints:   → wi 4  ∀wal 1523   ∈ wcel 2083  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892

This theorem depends on definitions:  df-bi 208  df-ral 3112

This theorem is referenced by:  ralimdva  3146  ssralv  3960  zorn2lem7  9777  pwfseqlem3  9935  sup2  11451  xrsupexmnf  12552  xrinfmexpnf  12553  xrsupsslem  12554  xrinfmsslem  12555  xrub  12559  r19.29uz  14548  rexuzre  14550  caurcvg  14871  caucvg  14873  isprm5  15884  prmgaplem5  16224  prmgaplem6  16225  mrissmrid  16745  elcls3  21379  iscnp4  21559  cncls2  21569  cnntr  21571  2ndcsep  21755  dyadmbllem  23887  xrlimcnp  25232  pntlem3  25871  sigaclfu2  30993  lfuhgr2  31975  rdgssun  34211  mapdordlem2  38325  dffltz  38789  iunrelexp0  39553  climrec  41447  0ellimcdiv  41493