Theorem ralimdv2 3150

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

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

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 3053

This theorem is referenced by:  ralimdva  3153  ssralvOLD  4036  zorn2lem7  10521  pwfseqlem3  10679  sup2  12203  xrsupexmnf  13326  xrinfmexpnf  13327  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  r19.29uz  15374  rexuzre  15376  caurcvg  15698  caucvg  15700  isprm5  16731  prmgaplem5  17080  prmgaplem6  17081  mrissmrid  17658  elcls3  23026  iscnp4  23206  cncls2  23216  cnntr  23218  2ndcsep  23402  dyadmbllem  25557  xrlimcnp  26935  pntlem3  27577  fldextrspunlsplem  33719  sigaclfu2  34157  lfuhgr2  35146  rdgssun  37401  mapdordlem2  41661  aks6d1c1  42134  sn-sup2  42481  dffltz  42624  cantnfresb  43315  safesnsupfiub  43407  iunrelexp0  43693  climrec  45599  0ellimcdiv  45645  pgindnf  49547