Theorem ralimdv2 3142

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  3145  ssralvOLD  4019  zorn2lem7  10455  pwfseqlem3  10613  sup2  12139  xrsupexmnf  13265  xrinfmexpnf  13266  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  r19.29uz  15317  rexuzre  15319  caurcvg  15643  caucvg  15645  isprm5  16677  prmgaplem5  17026  prmgaplem6  17027  mrissmrid  17602  elcls3  22970  iscnp4  23150  cncls2  23160  cnntr  23162  2ndcsep  23346  dyadmbllem  25500  xrlimcnp  26878  pntlem3  27520  fldextrspunlsplem  33668  sigaclfu2  34111  lfuhgr2  35106  rdgssun  37366  mapdordlem2  41631  aks6d1c1  42104  sn-sup2  42479  dffltz  42622  cantnfresb  43313  safesnsupfiub  43405  iunrelexp0  43691  climrec  45601  0ellimcdiv  45647  pgindnf  49702