Theorem ralimdv2 3172

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  ralimdva  3175  tz7.48lem  8443  zorn2lem7  10573  pwfseqlem3  10738  sup2  12266  xrsupexmnf  13428  xrinfmexpnf  13429  xrsupsslem  13430  xrinfmsslem  13431  xrub  13435  r19.29uz  15511  rexuzre  15513  caurcvg  15837  caucvg  15839  isprm5  16876  prmgaplem5  17226  prmgaplem6  17227  mrissmrid  17808  elcls3  23394  iscnp4  23574  cncls2  23584  cnntr  23586  2ndcsep  23771  dyadmbllem  25913  xrlimcnp  27289  pntlem3  27929  lfuhgr2  29720  fldextrspunlsplem  34298  sigaclfu2  34746  rdgssun  38281  mapdordlem2  42674  aks6d1c1  43146  sn-sup2  43535  dffltz  43650  cantnfresb  44310  safesnsupfiub  44401  iunrelexp0  44687  climrec  46584  0ellimcdiv  46628  pgindnf  50778