Theorem ralimdv2 3138

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  ralimdva  3141  ssralvOLD  4008  zorn2lem7  10396  pwfseqlem3  10554  sup2  12081  xrsupexmnf  13207  xrinfmexpnf  13208  xrsupsslem  13209  xrinfmsslem  13210  xrub  13214  r19.29uz  15258  rexuzre  15260  caurcvg  15584  caucvg  15586  isprm5  16618  prmgaplem5  16967  prmgaplem6  16968  mrissmrid  17547  elcls3  22968  iscnp4  23148  cncls2  23158  cnntr  23160  2ndcsep  23344  dyadmbllem  25498  xrlimcnp  26876  pntlem3  27518  fldextrspunlsplem  33640  sigaclfu2  34088  lfuhgr2  35092  rdgssun  37352  mapdordlem2  41616  aks6d1c1  42089  sn-sup2  42464  dffltz  42607  cantnfresb  43297  safesnsupfiub  43389  iunrelexp0  43675  climrec  45584  0ellimcdiv  45630  pgindnf  49701