Theorem ralimdv2 3141

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralimdva  3144  ssralvOLD  4002  zorn2lem7  10393  pwfseqlem3  10551  sup2  12078  xrsupexmnf  13204  xrinfmexpnf  13205  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  r19.29uz  15258  rexuzre  15260  caurcvg  15584  caucvg  15586  isprm5  16618  prmgaplem5  16967  prmgaplem6  16968  mrissmrid  17547  elcls3  22998  iscnp4  23178  cncls2  23188  cnntr  23190  2ndcsep  23374  dyadmbllem  25527  xrlimcnp  26905  pntlem3  27547  fldextrspunlsplem  33686  sigaclfu2  34134  lfuhgr2  35163  rdgssun  37420  mapdordlem2  41684  aks6d1c1  42157  sn-sup2  42532  dffltz  42675  cantnfresb  43365  safesnsupfiub  43457  iunrelexp0  43743  climrec  45651  0ellimcdiv  45695  pgindnf  49756