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 40872
Description: Quantification restricted to a subclass for two quantifiers. ssralv 4035 for two quantifiers. The proof of ssralv2 40872 was automatically generated by minimizing the automatically translated proof of ssralv2VD 41207. 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 1915 . 2 𝑥(𝐴𝐵𝐶𝐷)
2 nfra1 3221 . 2 𝑥𝑥𝐵𝑦𝐷 𝜑
3 ssralv 4035 . . . . . 6 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
43adantr 483 . . . . 5 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
5 df-ral 3145 . . . . 5 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
64, 5syl6ib 253 . . . 4 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)))
7 sp 2182 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
86, 7syl6 35 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐷 𝜑)))
9 ssralv 4035 . . . 4 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
109adantl 484 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
118, 10syl6d 75 . 2 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐶 𝜑)))
121, 2, 11ralrimd 3220 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wal 1535  wcel 2114  wral 3140  wss 3938
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  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-in 3945  df-ss 3954
This theorem is referenced by:  ordelordALT  40878  ordelordALTVD  41208
  Copyright terms: Public domain W3C validator