Theorem ralimdv2 3162

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ral 3061

This theorem is referenced by:  ralimdva  3166  ssralvOLD  4055  zorn2lem7  10543  pwfseqlem3  10701  sup2  12225  xrsupexmnf  13348  xrinfmexpnf  13349  xrsupsslem  13350  xrinfmsslem  13351  xrub  13355  r19.29uz  15390  rexuzre  15392  caurcvg  15714  caucvg  15716  isprm5  16745  prmgaplem5  17094  prmgaplem6  17095  mrissmrid  17685  elcls3  23092  iscnp4  23272  cncls2  23282  cnntr  23284  2ndcsep  23468  dyadmbllem  25635  xrlimcnp  27012  pntlem3  27654  fldextrspunlsplem  33724  sigaclfu2  34123  lfuhgr2  35125  rdgssun  37380  mapdordlem2  41640  aks6d1c1  42118  sn-sup2  42506  dffltz  42649  cantnfresb  43342  safesnsupfiub  43434  iunrelexp0  43720  climrec  45623  0ellimcdiv  45669  pgindnf  49290