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 39409
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3826 for two quantifiers. The proof of ssralv2 39409 was automatically generated by minimizing the automatically translated proof of ssralv2VD 39754. The automatic translation is by the tools program translatewithout_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 2009 . 2 𝑥(𝐴𝐵𝐶𝐷)
2 nfra1 3088 . 2 𝑥𝑥𝐵𝑦𝐷 𝜑
3 ssralv 3826 . . . . . 6 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
43adantr 472 . . . . 5 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
5 df-ral 3060 . . . . 5 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
64, 5syl6ib 242 . . . 4 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)))
7 sp 2215 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
86, 7syl6 35 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐷 𝜑)))
9 ssralv 3826 . . . 4 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
109adantl 473 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
118, 10syl6d 75 . 2 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐶 𝜑)))
121, 2, 11ralrimd 3106 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1650  wcel 2155  wral 3055  wss 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ral 3060  df-in 3739  df-ss 3746
This theorem is referenced by:  ordelordALT  39415  ordelordALTVD  39755
  Copyright terms: Public domain W3C validator