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 38205
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3650 for two quantifiers. The proof of ssralv2 38205 was automatically generated by minimizing the automatically translated proof of ssralv2VD 38571. 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 1845 . 2 𝑥(𝐴𝐵𝐶𝐷)
2 nfra1 2941 . 2 𝑥𝑥𝐵𝑦𝐷 𝜑
3 ssralv 3650 . . . . . 6 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
43adantr 481 . . . . 5 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
5 df-ral 2917 . . . . 5 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
64, 5syl6ib 241 . . . 4 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)))
7 sp 2056 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
86, 7syl6 35 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐷 𝜑)))
9 ssralv 3650 . . . 4 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
109adantl 482 . . 3 ((𝐴𝐵𝐶𝐷) → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
118, 10syl6d 75 . 2 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → (𝑥𝐴 → ∀𝑦𝐶 𝜑)))
121, 2, 11ralrimd 2958 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1478  wcel 1992  wral 2912  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-ral 2917  df-in 3567  df-ss 3574
This theorem is referenced by:  ordelordALT  38215  ordelordALTVD  38572
  Copyright terms: Public domain W3C validator