![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > onfrALTlem4VD | Structured version Visualization version GIF version |
Description: Virtual deduction proof of onfrALTlem4 43289.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem4 43289 is onfrALTlem4VD 43632 without virtual deductions and was
automatically derived from onfrALTlem4VD 43632.
|
Ref | Expression |
---|---|
onfrALTlem4VD | ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcan 3828 | . 2 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅)) | |
2 | sbcel1v 3847 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎) | |
3 | sbceqg 4408 | . . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)) | |
4 | 3 | elv 3480 | . . . 4 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅) |
5 | csbin 4438 | . . . . . 6 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) | |
6 | csbconstg 3911 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑎 = 𝑎) | |
7 | 6 | elv 3480 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎 |
8 | vex 3478 | . . . . . . . 8 ⊢ 𝑦 ∈ V | |
9 | 8 | csbvargi 4431 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
10 | 7, 9 | ineq12i 4209 | . . . . . 6 ⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = (𝑎 ∩ 𝑦) |
11 | 5, 10 | eqtri 2760 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦) |
12 | csb0 4406 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌∅ = ∅ | |
13 | 11, 12 | eqeq12i 2750 | . . . 4 ⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
14 | 4, 13 | bitri 274 | . . 3 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
15 | 2, 14 | anbi12i 627 | . 2 ⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
16 | 1, 15 | bitri 274 | 1 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 Vcvv 3474 [wsbc 3776 ⦋csb 3892 ∩ cin 3946 ∅c0 4321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-in 3954 df-nul 4322 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |