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  4049  zorn2lem7  10493  pwfseqlem3  10651  sup2  12166  xrsupexmnf  13280  xrinfmexpnf  13281  xrsupsslem  13282  xrinfmsslem  13283  xrub  13287  r19.29uz  15293  rexuzre  15295  caurcvg  15619  caucvg  15621  isprm5  16640  prmgaplem5  16984  prmgaplem6  16985  mrissmrid  17581  elcls3  22578  iscnp4  22758  cncls2  22768  cnntr  22770  2ndcsep  22954  dyadmbllem  25107  xrlimcnp  26462  pntlem3  27101  sigaclfu2  33107  lfuhgr2  34097  rdgssun  36247  mapdordlem2  40496  sn-sup2  41338  dffltz  41372  cantnfresb  42059  safesnsupfiub  42152  iunrelexp0  42438  climrec  44305  0ellimcdiv  44351  pgindnf  47714