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 44859
Description: Virtual deduction proof of onfrALTlem4 44516. 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 44516 is onfrALTlem4VD 44859 without virtual deductions and was automatically derived from onfrALTlem4VD 44859.
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 3857 . 2 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅))
2 sbcel1v 3875 . . 3 ([𝑦 / 𝑥]𝑥𝑎𝑦𝑎)
3 sbceqg 4435 . . . . 5 (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅))
43elv 3493 . . . 4 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ 𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅)
5 csbin 4465 . . . . . 6 𝑦 / 𝑥(𝑎𝑥) = (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥)
6 csbconstg 3940 . . . . . . . 8 (𝑦 ∈ V → 𝑦 / 𝑥𝑎 = 𝑎)
76elv 3493 . . . . . . 7 𝑦 / 𝑥𝑎 = 𝑎
8 vex 3492 . . . . . . . 8 𝑦 ∈ V
98csbvargi 4458 . . . . . . 7 𝑦 / 𝑥𝑥 = 𝑦
107, 9ineq12i 4239 . . . . . 6 (𝑦 / 𝑥𝑎𝑦 / 𝑥𝑥) = (𝑎𝑦)
115, 10eqtri 2768 . . . . 5 𝑦 / 𝑥(𝑎𝑥) = (𝑎𝑦)
12 csb0 4433 . . . . 5 𝑦 / 𝑥∅ = ∅
1311, 12eqeq12i 2758 . . . 4 (𝑦 / 𝑥(𝑎𝑥) = 𝑦 / 𝑥∅ ↔ (𝑎𝑦) = ∅)
144, 13bitri 275 . . 3 ([𝑦 / 𝑥](𝑎𝑥) = ∅ ↔ (𝑎𝑦) = ∅)
152, 14anbi12i 627 . 2 (([𝑦 / 𝑥]𝑥𝑎[𝑦 / 𝑥](𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
161, 15bitri 275 1 ([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  Vcvv 3488  [wsbc 3804  csb 3921  cin 3975  c0 4352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-in 3983  df-nul 4353
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator