| 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 44526.
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 44526 is onfrALTlem4VD 44868 without virtual deductions and was
automatically derived from onfrALTlem4VD 44868.
|
| Ref | Expression |
|---|---|
| onfrALTlem4VD | ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcan 3805 | . 2 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅)) | |
| 2 | sbcel1v 3821 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎) | |
| 3 | sbceqg 4377 | . . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)) | |
| 4 | 3 | elv 3455 | . . . 4 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅) |
| 5 | csbin 4407 | . . . . . 6 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) | |
| 6 | csbconstg 3883 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑎 = 𝑎) | |
| 7 | 6 | elv 3455 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎 |
| 8 | vex 3454 | . . . . . . . 8 ⊢ 𝑦 ∈ V | |
| 9 | 8 | csbvargi 4400 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
| 10 | 7, 9 | ineq12i 4183 | . . . . . 6 ⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = (𝑎 ∩ 𝑦) |
| 11 | 5, 10 | eqtri 2753 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦) |
| 12 | csb0 4375 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌∅ = ∅ | |
| 13 | 11, 12 | eqeq12i 2748 | . . . 4 ⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
| 14 | 4, 13 | bitri 275 | . . 3 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
| 15 | 2, 14 | anbi12i 628 | . 2 ⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
| 16 | 1, 15 | bitri 275 | 1 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 Vcvv 3450 [wsbc 3755 ⦋csb 3864 ∩ cin 3915 ∅c0 4298 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-in 3923 df-nul 4299 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |