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

Syntax hints:   → wi 4  ∀wal 1558   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ral 3077

This theorem is referenced by:  ralimdva  3174  zorn2lem7  10459  pwfseqlem3  10618  sup2  12148  xrsupexmnf  13308  xrinfmexpnf  13309  xrsupsslem  13310  xrinfmsslem  13311  xrub  13315  r19.29uz  15378  rexuzre  15380  caurcvg  15704  caucvg  15706  isprm5  16742  prmgaplem5  17091  prmgaplem6  17092  mrissmrid  17673  elcls3  23140  iscnp4  23320  cncls2  23330  cnntr  23332  2ndcsep  23516  dyadmbllem  25658  xrlimcnp  27030  pntlem3  27670  fldextrspunlsplem  33967  sigaclfu2  34415  lfuhgr2  35466  rdgssun  37869  mapdordlem2  42258  aks6d1c1  42730  sn-sup2  43110  dffltz  43213  cantnfresb  43898  safesnsupfiub  43989  iunrelexp0  44275  climrec  46176  0ellimcdiv  46220  pgindnf  50334