Theorem ralimdv2 3180

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

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

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

This theorem is referenced by:  ralimdva  3183  zorn2lem7  10485  pwfseqlem3  10644  sup2  12170  xrsupexmnf  13330  xrinfmexpnf  13331  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  r19.29uz  15401  rexuzre  15403  caurcvg  15727  caucvg  15729  isprm5  16765  prmgaplem5  17114  prmgaplem6  17115  mrissmrid  17696  elcls3  23208  iscnp4  23388  cncls2  23398  cnntr  23400  2ndcsep  23584  dyadmbllem  25726  xrlimcnp  27098  pntlem3  27738  fldextrspunlsplem  34007  sigaclfu2  34455  lfuhgr2  35509  rdgssun  37911  mapdordlem2  42300  aks6d1c1  42772  sn-sup2  43154  dffltz  43257  cantnfresb  43942  safesnsupfiub  44033  iunrelexp0  44319  climrec  46210  0ellimcdiv  46254  pgindnf  50378