Theorem ralimdv2 3146

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ralimdva  3149  ssralvOLD  3994  zorn2lem7  10424  pwfseqlem3  10583  sup2  12112  xrsupexmnf  13257  xrinfmexpnf  13258  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  r19.29uz  15313  rexuzre  15315  caurcvg  15639  caucvg  15641  isprm5  16677  prmgaplem5  17026  prmgaplem6  17027  mrissmrid  17607  elcls3  23048  iscnp4  23228  cncls2  23238  cnntr  23240  2ndcsep  23424  dyadmbllem  25566  xrlimcnp  26932  pntlem3  27572  fldextrspunlsplem  33817  sigaclfu2  34265  lfuhgr2  35301  rdgssun  37694  mapdordlem2  42083  aks6d1c1  42555  sn-sup2  42936  dffltz  43067  cantnfresb  43752  safesnsupfiub  43843  iunrelexp0  44129  climrec  46033  0ellimcdiv  46077  pgindnf  50191