Theorem ralimdv2 3147

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 1912

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

This theorem is referenced by:  ralimdva  3150  ssralvOLD  4008  zorn2lem7  10424  pwfseqlem3  10583  sup2  12110  xrsupexmnf  13232  xrinfmexpnf  13233  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  r19.29uz  15286  rexuzre  15288  caurcvg  15612  caucvg  15614  isprm5  16646  prmgaplem5  16995  prmgaplem6  16996  mrissmrid  17576  elcls3  23039  iscnp4  23219  cncls2  23229  cnntr  23231  2ndcsep  23415  dyadmbllem  25568  xrlimcnp  26946  pntlem3  27588  fldextrspunlsplem  33851  sigaclfu2  34299  lfuhgr2  35335  rdgssun  37633  mapdordlem2  42013  aks6d1c1  42486  sn-sup2  42861  dffltz  42992  cantnfresb  43681  safesnsupfiub  43772  iunrelexp0  44058  climrec  45963  0ellimcdiv  46007  pgindnf  50075