Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eusvobj2 Structured version   Visualization version   Unicode version

Theorem eusvobj2 6283
 Description: Specify the same property in two ways when class is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
Hypothesis
Ref Expression
eusvobj1.1
Assertion
Ref Expression
eusvobj2
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem eusvobj2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 euabsn2 4043 . . 3
2 eleq2 2518 . . . . . 6
3 abid 2439 . . . . . 6
4 elsn 3982 . . . . . 6
52, 3, 43bitr3g 291 . . . . 5
6 nfre1 2848 . . . . . . . . 9
76nfab 2596 . . . . . . . 8
87nfeq1 2605 . . . . . . 7
9 eusvobj1.1 . . . . . . . . 9
109elabrex 6148 . . . . . . . 8
11 eleq2 2518 . . . . . . . . 9
129elsnc 3992 . . . . . . . . . 10
13 eqcom 2458 . . . . . . . . . 10
1412, 13bitri 253 . . . . . . . . 9
1511, 14syl6bb 265 . . . . . . . 8
1610, 15syl5ib 223 . . . . . . 7
178, 16ralrimi 2788 . . . . . 6
18 eqeq1 2455 . . . . . . 7
1918ralbidv 2827 . . . . . 6
2017, 19syl5ibrcom 226 . . . . 5
215, 20sylbid 219 . . . 4
2221exlimiv 1776 . . 3
231, 22sylbi 199 . 2
24 euex 2323 . . 3
25 rexn0 3872 . . . 4
2625exlimiv 1776 . . 3
27 r19.2z 3858 . . . 4
2827ex 436 . . 3
2924, 26, 283syl 18 . 2
3023, 29impbid 194 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wceq 1444  wex 1663   wcel 1887  weu 2299  cab 2437   wne 2622  wral 2737  wrex 2738  cvv 3045  c0 3731  csn 3968 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-nul 3732  df-sn 3969 This theorem is referenced by:  eusvobj1  6284
 Copyright terms: Public domain W3C validator