Theorem ralimdv2 3169

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  ralimdva  3173  ssralvOLD  4081  zorn2lem7  10571  pwfseqlem3  10729  sup2  12251  xrsupexmnf  13367  xrinfmexpnf  13368  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  r19.29uz  15399  rexuzre  15401  caurcvg  15725  caucvg  15727  isprm5  16754  prmgaplem5  17102  prmgaplem6  17103  mrissmrid  17699  elcls3  23112  iscnp4  23292  cncls2  23302  cnntr  23304  2ndcsep  23488  dyadmbllem  25653  xrlimcnp  27029  pntlem3  27671  sigaclfu2  34085  lfuhgr2  35086  rdgssun  37344  mapdordlem2  41594  aks6d1c1  42073  sn-sup2  42447  dffltz  42589  cantnfresb  43286  safesnsupfiub  43378  iunrelexp0  43664  climrec  45524  0ellimcdiv  45570  pgindnf  48808