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

Theorem onfrALTlem4VD 39621
Description: Virtual deduction proof of onfrALTlem4 39260. 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 39260 is onfrALTlem4VD 39621 without virtual deductions and was automatically derived from onfrALTlem4VD 39621.
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 vex 3343 . . 3 𝑦 ∈ V
2 sbcangOLD 39241 . . 3 (𝑦 ∈ V → ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅)))
31, 2e0a 39501 . 2 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅))
4 sbcel1gvOLD 39593 . . . 4 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥𝑎𝑦𝑎))
51, 4e0a 39501 . . 3 ([𝑦 / 𝑥]𝑥𝑎𝑦𝑎)
6 sbceqg 4127 . . . . 5 (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅))
71, 6e0a 39501 . . . 4 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅)
8 csbingOLD 39554 . . . . . . 7 (𝑦 ∈ V → 𝑦 / 𝑥(𝑎𝑥) = (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥))
91, 8e0a 39501 . . . . . 6 𝑦 / 𝑥(𝑎𝑥) = (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥)
10 csbconstg 3687 . . . . . . . 8 (𝑦 ∈ V → 𝑦 / 𝑥𝑎 = 𝑎)
111, 10e0a 39501 . . . . . . 7 𝑦 / 𝑥𝑎 = 𝑎
12 csbvarg 4146 . . . . . . . 8 (𝑦 ∈ V → 𝑦 / 𝑥𝑥 = 𝑦)
131, 12e0a 39501 . . . . . . 7 𝑦 / 𝑥𝑥 = 𝑦
1411, 13ineq12i 3955 . . . . . 6 (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥) = (𝑎𝑦)
159, 14eqtri 2782 . . . . 5 𝑦 / 𝑥(𝑎𝑥) = (𝑎𝑦)
16 csbconstg 3687 . . . . . 6 (𝑦 ∈ V → 𝑦 / 𝑥∅ = ∅)
171, 16e0a 39501 . . . . 5 𝑦 / 𝑥∅ = ∅
1815, 17eqeq12i 2774 . . . 4 (𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅ ↔ (𝑎𝑦) = ∅)
197, 18bitri 264 . . 3 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ (𝑎𝑦) = ∅)
205, 19anbi12i 735 . 2 (([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
213, 20bitri 264 1 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  wcel 2139  Vcvv 3340  [wsbc 3576  csb 3674  cin 3714  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-in 3722
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator