Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssralv2 Structured version   Visualization version   GIF version

Theorem ssralv2 44529
Description: Quantification restricted to a subclass for two quantifiers. ssralv 4064 for two quantifiers. The proof of ssralv2 44529 was automatically generated by minimizing the automatically translated proof of ssralv2VD 44864. The automatic translation is by the tools program translate_without_overwriting.cmd. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ssralv2 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑦,𝐶   𝑥,𝐷   𝑦,𝐷
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem ssralv2
StepHypRef Expression
1 nfv 1912 . 2 𝑥(𝐴𝐵𝐶𝐷)
2 nfra1 3282 . 2 𝑥𝑥𝐵𝑦𝐷 𝜑
3 ssralv 4064 . . . . . 6 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
43adantr 480 . . . . 5 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
5 df-ral 3060 . . . . 5 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
64, 5imbitrdi 251 . . . 4 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)))
7 sp 2181 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
86, 7syl6 35 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐷 𝜑)))
9 ssralv 4064 . . . 4 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
109adantl 481 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
118, 10syl6d 75 . 2 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐶 𝜑)))
121, 2, 11ralrimd 3262 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1535  wcel 2106  wral 3059  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-ral 3060  df-ss 3980
This theorem is referenced by:  ordelordALT  44535  ordelordALTVD  44865
  Copyright terms: Public domain W3C validator