![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbc2or | Structured version Visualization version GIF 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 3701 (false) and sbc6 3703 (true) conclusions. This is interesting since dfsbcq 3678 and dfsbcq2 3679 (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 3679 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
2 | eqeq2 2784 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) | |
3 | 2 | anbi1d 621 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ 𝜑))) |
4 | 3 | exbidv 1881 | . . . 4 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
5 | sb5 2206 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
6 | 1, 4, 5 | vtoclbg 3482 | . . 3 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
7 | 6 | orcd 860 | . 2 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))) |
8 | pm5.15 996 | . . 3 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) | |
9 | vex 3413 | . . . . . . . . . 10 ⊢ 𝑥 ∈ V | |
10 | eleq1 2848 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
11 | 9, 10 | mpbii 225 | . . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
12 | 11 | adantr 473 | . . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝐴 ∈ V) |
13 | 12 | con3i 152 | . . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑥 = 𝐴 ∧ 𝜑)) |
14 | 13 | nexdv 1896 | . . . . . 6 ⊢ (¬ 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
15 | 11 | con3i 152 | . . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑥 = 𝐴) |
16 | 15 | pm2.21d 119 | . . . . . . 7 ⊢ (¬ 𝐴 ∈ V → (𝑥 = 𝐴 → 𝜑)) |
17 | 16 | alrimiv 1887 | . . . . . 6 ⊢ (¬ 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴 → 𝜑)) |
18 | 14, 17 | 2thd 257 | . . . . 5 ⊢ (¬ 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) |
19 | 18 | bibi2d 335 | . . . 4 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))) |
20 | 19 | orbi2d 900 | . . 3 ⊢ (¬ 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))) |
21 | 8, 20 | mpbii 225 | . 2 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))) |
22 | 7, 21 | pm2.61i 177 | 1 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∨ wo 834 ∀wal 1506 = wceq 1508 ∃wex 1743 [wsb 2016 ∈ wcel 2051 Vcvv 3410 [wsbc 3676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-12 2107 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-v 3412 df-sbc 3677 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |