Theorem ralimdv2 3163

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  ∀wral 3061

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 1913

This theorem depends on definitions:  df-bi 206  df-ral 3062

This theorem is referenced by:  ralimdva  3167  ssralv  4050  zorn2lem7  10499  pwfseqlem3  10657  sup2  12172  xrsupexmnf  13286  xrinfmexpnf  13287  xrsupsslem  13288  xrinfmsslem  13289  xrub  13293  r19.29uz  15299  rexuzre  15301  caurcvg  15625  caucvg  15627  isprm5  16646  prmgaplem5  16990  prmgaplem6  16991  mrissmrid  17587  elcls3  22594  iscnp4  22774  cncls2  22784  cnntr  22786  2ndcsep  22970  dyadmbllem  25123  xrlimcnp  26480  pntlem3  27119  sigaclfu2  33188  lfuhgr2  34178  rdgssun  36345  mapdordlem2  40594  sn-sup2  41424  dffltz  41458  cantnfresb  42156  safesnsupfiub  42249  iunrelexp0  42535  climrec  44398  0ellimcdiv  44444  pgindnf  47839