Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-equsb3 Structured version   Visualization version   Unicode version

Theorem wl-equsb3 31954
Description: equsb3 2281 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
Assertion
Ref Expression
wl-equsb3  |-  ( -. 
A. y  y  =  z  ->  ( [
x  /  y ] y  =  z  <->  x  =  z ) )

Proof of Theorem wl-equsb3
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 nfv 1769 . . 3  |-  F/ w  -.  A. y  y  =  z
2 nfna1 2005 . . . 4  |-  F/ y  -.  A. y  y  =  z
3 nfeqf2 2148 . . . 4  |-  ( -. 
A. y  y  =  z  ->  F/ y  w  =  z )
4 equequ1 1875 . . . . 5  |-  ( y  =  w  ->  (
y  =  z  <->  w  =  z ) )
54a1i 11 . . . 4  |-  ( -. 
A. y  y  =  z  ->  ( y  =  w  ->  ( y  =  z  <->  w  =  z ) ) )
62, 3, 5sbied 2258 . . 3  |-  ( -. 
A. y  y  =  z  ->  ( [
w  /  y ] y  =  z  <->  w  =  z ) )
71, 6sbbid 2252 . 2  |-  ( -. 
A. y  y  =  z  ->  ( [
x  /  w ] [ w  /  y ] y  =  z  <->  [ x  /  w ] w  =  z
) )
8 sbcom3 2260 . . 3  |-  ( [ x  /  w ] [ w  /  y ] y  =  z  <->  [ x  /  w ] [ x  /  y ] y  =  z )
9 nfv 1769 . . . 4  |-  F/ w [ x  /  y ] y  =  z
109sbf 2229 . . 3  |-  ( [ x  /  w ] [ x  /  y ] y  =  z  <->  [ x  /  y ] y  =  z )
118, 10bitri 257 . 2  |-  ( [ x  /  w ] [ w  /  y ] y  =  z  <->  [ x  /  y ] y  =  z )
12 equsb3 2281 . 2  |-  ( [ x  /  w ]
w  =  z  <->  x  =  z )
137, 11, 123bitr3g 295 1  |-  ( -. 
A. y  y  =  z  ->  ( [
x  /  y ] y  =  z  <->  x  =  z ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189   A.wal 1450   [wsb 1805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-13 2104
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator