Theorem ralimdv2 3161

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  ralimdva  3165  ssralvOLD  4068  zorn2lem7  10540  pwfseqlem3  10698  sup2  12222  xrsupexmnf  13344  xrinfmexpnf  13345  xrsupsslem  13346  xrinfmsslem  13347  xrub  13351  r19.29uz  15386  rexuzre  15388  caurcvg  15710  caucvg  15712  isprm5  16741  prmgaplem5  17089  prmgaplem6  17090  mrissmrid  17686  elcls3  23107  iscnp4  23287  cncls2  23297  cnntr  23299  2ndcsep  23483  dyadmbllem  25648  xrlimcnp  27026  pntlem3  27668  sigaclfu2  34102  lfuhgr2  35103  rdgssun  37361  mapdordlem2  41620  aks6d1c1  42098  sn-sup2  42478  dffltz  42621  cantnfresb  43314  safesnsupfiub  43406  iunrelexp0  43692  climrec  45559  0ellimcdiv  45605  pgindnf  48947