Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbc2or | Structured version Visualization version Unicode version |
Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis. This theorem tells us that there are only 2 possibilities for behavior at proper classes, matching the sbc5 3460 (false) and sbc6 3462 (true) conclusions. This is interesting since dfsbcq 3437 and dfsbcq2 3438 (from which it is derived) do not appear to say anything obvious about proper class behavior. Note that this theorem does not tell us that it is always one or the other at proper classes; it could "flip" between false (the first disjunct) and true (the second disjunct) as a function of some other variable that or may contain. (Contributed by NM, 11-Oct-2004.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbc2or |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq2 3438 | . . . 4 | |
2 | eqeq2 2633 | . . . . . 6 | |
3 | 2 | anbi1d 741 | . . . . 5 |
4 | 3 | exbidv 1850 | . . . 4 |
5 | sb5 2430 | . . . 4 | |
6 | 1, 4, 5 | vtoclbg 3267 | . . 3 |
7 | 6 | orcd 407 | . 2 |
8 | pm5.15 933 | . . 3 | |
9 | vex 3203 | . . . . . . . . . 10 | |
10 | eleq1 2689 | . . . . . . . . . 10 | |
11 | 9, 10 | mpbii 223 | . . . . . . . . 9 |
12 | 11 | adantr 481 | . . . . . . . 8 |
13 | 12 | con3i 150 | . . . . . . 7 |
14 | 13 | nexdv 1864 | . . . . . 6 |
15 | 11 | con3i 150 | . . . . . . . 8 |
16 | 15 | pm2.21d 118 | . . . . . . 7 |
17 | 16 | alrimiv 1855 | . . . . . 6 |
18 | 14, 17 | 2thd 255 | . . . . 5 |
19 | 18 | bibi2d 332 | . . . 4 |
20 | 19 | orbi2d 738 | . . 3 |
21 | 8, 20 | mpbii 223 | . 2 |
22 | 7, 21 | pm2.61i 176 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wo 383 wa 384 wal 1481 wceq 1483 wex 1704 wsb 1880 wcel 1990 cvv 3200 wsbc 3435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-sbc 3436 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |