Theorem ralimdv2 3157

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

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

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 3063

This theorem is referenced by:  ralimdva  3161  ssralv  4001  zorn2lem7  10363  pwfseqlem3  10521  sup2  12036  xrsupexmnf  13144  xrinfmexpnf  13145  xrsupsslem  13146  xrinfmsslem  13147  xrub  13151  r19.29uz  15161  rexuzre  15163  caurcvg  15487  caucvg  15489  isprm5  16509  prmgaplem5  16853  prmgaplem6  16854  mrissmrid  17447  elcls3  22339  iscnp4  22519  cncls2  22529  cnntr  22531  2ndcsep  22715  dyadmbllem  24868  xrlimcnp  26223  pntlem3  26862  sigaclfu2  32385  lfuhgr2  33377  rdgssun  35703  mapdordlem2  39956  sn-sup2  40750  dffltz  40784  safesnsupfiub  41397  iunrelexp0  41683  climrec  43532  0ellimcdiv  43578