Theorem ralimdv2 3141

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralimdva  3144  ssralvOLD  4002  zorn2lem7  10399  pwfseqlem3  10557  sup2  12084  xrsupexmnf  13210  xrinfmexpnf  13211  xrsupsslem  13212  xrinfmsslem  13213  xrub  13217  r19.29uz  15264  rexuzre  15266  caurcvg  15590  caucvg  15592  isprm5  16624  prmgaplem5  16973  prmgaplem6  16974  mrissmrid  17553  elcls3  23004  iscnp4  23184  cncls2  23194  cnntr  23196  2ndcsep  23380  dyadmbllem  25533  xrlimcnp  26911  pntlem3  27553  fldextrspunlsplem  33693  sigaclfu2  34141  lfuhgr2  35170  rdgssun  37429  mapdordlem2  41742  aks6d1c1  42215  sn-sup2  42590  dffltz  42733  cantnfresb  43422  safesnsupfiub  43514  iunrelexp0  43800  climrec  45708  0ellimcdiv  45752  pgindnf  49822