Theorem ralimdv2 3149

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

Syntax hints:   → wi 4  ∀wal 1635   ∈ wcel 2156  ∀wral 3096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001

This theorem depends on definitions:  df-bi 198  df-ral 3101

This theorem is referenced by:  ralimdva  3150  ssralv  3863  zorn2lem7  9609  pwfseqlem3  9767  sup2  11264  xrsupexmnf  12353  xrinfmexpnf  12354  xrsupsslem  12355  xrinfmsslem  12356  xrub  12360  r19.29uz  14313  rexuzre  14315  caurcvg  14630  caucvg  14632  isprm5  15636  prmgaplem5  15976  prmgaplem6  15977  mrissmrid  16506  elcls3  21101  iscnp4  21281  cncls2  21291  cnntr  21293  2ndcsep  21476  dyadmbllem  23580  xrlimcnp  24909  pntlem3  25512  sigaclfu2  30509  mapdordlem2  37418  iunrelexp0  38494  climrec  40315  0ellimcdiv  40361