Theorem ralimdv2 3142

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralimdva  3145  ssralvOLD  4016  zorn2lem7  10431  pwfseqlem3  10589  sup2  12115  xrsupexmnf  13241  xrinfmexpnf  13242  xrsupsslem  13243  xrinfmsslem  13244  xrub  13248  r19.29uz  15293  rexuzre  15295  caurcvg  15619  caucvg  15621  isprm5  16653  prmgaplem5  17002  prmgaplem6  17003  mrissmrid  17578  elcls3  22946  iscnp4  23126  cncls2  23136  cnntr  23138  2ndcsep  23322  dyadmbllem  25476  xrlimcnp  26854  pntlem3  27496  fldextrspunlsplem  33641  sigaclfu2  34084  lfuhgr2  35079  rdgssun  37339  mapdordlem2  41604  aks6d1c1  42077  sn-sup2  42452  dffltz  42595  cantnfresb  43286  safesnsupfiub  43378  iunrelexp0  43664  climrec  45574  0ellimcdiv  45620  pgindnf  49678