Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onfrALTlem4VD Structured version   Visualization version   GIF version

Theorem onfrALTlem4VD 41993
Description: Virtual deduction proof of onfrALTlem4 41650. 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 41650 is onfrALTlem4VD 41993 without virtual deductions and was automatically derived from onfrALTlem4VD 41993.
 1:: ⊢ 𝑦 ∈ V 2:1: ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋ 𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅) 3:1: ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌ 𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) 4:1: ⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎 5:1: ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 6:4,5: ⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = ( 𝑎 ∩ 𝑦) 7:3,6: ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦) 8:1: ⊢ ⦋𝑦 / 𝑥⦌∅ = ∅ 9:7,8: ⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌ ∅ ↔ (𝑎 ∩ 𝑦) = ∅) 10:2,9: ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅) 11:1: ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎) 12:11,10: ⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥]( 𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) 13:1: ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅)) qed:13,12: ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem4VD ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
Distinct variable group:   𝑥,𝑎

Proof of Theorem onfrALTlem4VD
StepHypRef Expression
1 sbcan 3747 . 2 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅))
2 sbcel1v 3765 . . 3 ([𝑦 / 𝑥]𝑥𝑎𝑦𝑎)
3 sbceqg 4309 . . . . 5 (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅))
43elv 3415 . . . 4 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅)
5 csbin 4339 . . . . . 6 𝑦 / 𝑥(𝑎𝑥) = (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥)
6 csbconstg 3826 . . . . . . . 8 (𝑦 ∈ V → 𝑦 / 𝑥𝑎 = 𝑎)
76elv 3415 . . . . . . 7 𝑦 / 𝑥𝑎 = 𝑎
8 vex 3413 . . . . . . . 8 𝑦 ∈ V
98csbvargi 4332 . . . . . . 7 𝑦 / 𝑥𝑥 = 𝑦
107, 9ineq12i 4117 . . . . . 6 (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥) = (𝑎𝑦)
115, 10eqtri 2781 . . . . 5 𝑦 / 𝑥(𝑎𝑥) = (𝑎𝑦)
12 csb0 4306 . . . . 5 𝑦 / 𝑥∅ = ∅
1311, 12eqeq12i 2773 . . . 4 (𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅ ↔ (𝑎𝑦) = ∅)
144, 13bitri 278 . . 3 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ (𝑎𝑦) = ∅)
152, 14anbi12i 629 . 2 (([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
161, 15bitri 278 1 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  Vcvv 3409  [wsbc 3698  ⦋csb 3807   ∩ cin 3859  ∅c0 4227 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-in 3867  df-nul 4228 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator