ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eusvobj2 Structured version   GIF version

Theorem eusvobj2 5422
Description: Specify the same property in two ways when class B(y) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
Hypothesis
Ref Expression
eusvobj1.1 B V
Assertion
Ref Expression
eusvobj2 (∃!xy A x = B → (y A x = By A x = B))
Distinct variable groups:   x,y,A   x,B
Allowed substitution hint:   B(y)

Proof of Theorem eusvobj2
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 euabsn2 3413 . . 3 (∃!xy A x = Bz{xy A x = B} = {z})
2 eleq2 2083 . . . . . 6 ({xy A x = B} = {z} → (x {xy A x = B} ↔ x {z}))
3 abid 2010 . . . . . 6 (x {xy A x = B} ↔ y A x = B)
4 elsn 3365 . . . . . 6 (x {z} ↔ x = z)
52, 3, 43bitr3g 211 . . . . 5 ({xy A x = B} = {z} → (y A x = Bx = z))
6 nfre1 2343 . . . . . . . . 9 yy A x = B
76nfab 2164 . . . . . . . 8 y{xy A x = B}
87nfeq1 2169 . . . . . . 7 y{xy A x = B} = {z}
9 eusvobj1.1 . . . . . . . . 9 B V
109elabrex 5322 . . . . . . . 8 (y AB {xy A x = B})
11 eleq2 2083 . . . . . . . . 9 ({xy A x = B} = {z} → (B {xy A x = B} ↔ B {z}))
129elsnc 3373 . . . . . . . . . 10 (B {z} ↔ B = z)
13 eqcom 2024 . . . . . . . . . 10 (B = zz = B)
1412, 13bitri 173 . . . . . . . . 9 (B {z} ↔ z = B)
1511, 14syl6bb 185 . . . . . . . 8 ({xy A x = B} = {z} → (B {xy A x = B} ↔ z = B))
1610, 15syl5ib 143 . . . . . . 7 ({xy A x = B} = {z} → (y Az = B))
178, 16ralrimi 2368 . . . . . 6 ({xy A x = B} = {z} → y A z = B)
18 eqeq1 2028 . . . . . . 7 (x = z → (x = Bz = B))
1918ralbidv 2304 . . . . . 6 (x = z → (y A x = By A z = B))
2017, 19syl5ibrcom 146 . . . . 5 ({xy A x = B} = {z} → (x = zy A x = B))
215, 20sylbid 139 . . . 4 ({xy A x = B} = {z} → (y A x = By A x = B))
2221exlimiv 1471 . . 3 (z{xy A x = B} = {z} → (y A x = By A x = B))
231, 22sylbi 114 . 2 (∃!xy A x = B → (y A x = By A x = B))
24 euex 1912 . . 3 (∃!xy A x = Bxy A x = B)
25 rexm 3299 . . . 4 (y A x = By y A)
2625exlimiv 1471 . . 3 (xy A x = By y A)
27 r19.2m 3286 . . . 4 ((y y A y A x = B) → y A x = B)
2827ex 108 . . 3 (y y A → (y A x = By A x = B))
2924, 26, 283syl 17 . 2 (∃!xy A x = B → (y A x = By A x = B))
3023, 29impbid 120 1 (∃!xy A x = B → (y A x = By A x = B))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1228  wex 1362   wcel 1374  ∃!weu 1882  {cab 2008  wral 2284  wrex 2285  Vcvv 2535  {csn 3350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-v 2537  df-sbc 2742  df-csb 2830  df-sn 3356
This theorem is referenced by:  eusvobj1  5423
  Copyright terms: Public domain W3C validator