Theorem ralimdv2 3174

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

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  ralimdva  3177  zorn2lem7  10481  pwfseqlem3  10640  sup2  12166  xrsupexmnf  13326  xrinfmexpnf  13327  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  r19.29uz  15398  rexuzre  15400  caurcvg  15724  caucvg  15726  isprm5  16761  prmgaplem5  17110  prmgaplem6  17111  mrissmrid  17692  elcls3  23240  iscnp4  23420  cncls2  23430  cnntr  23432  2ndcsep  23616  dyadmbllem  25758  xrlimcnp  27133  pntlem3  27773  fldextrspunlsplem  34063  sigaclfu2  34511  lfuhgr2  35611  rdgssun  38024  mapdordlem2  42411  aks6d1c1  42883  sn-sup2  43265  dffltz  43366  cantnfresb  44051  safesnsupfiub  44142  iunrelexp0  44428  climrec  46319  0ellimcdiv  46363  pgindnf  50494