Theorem eusvobj2 5441

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 e. _V

Assertion

Ref	Expression
eusvobj2	|- (E!xE.y e. A x = B -> (E.y e. A x = B <-> A.y e. 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.

Step	Hyp	Ref	Expression
1		euabsn2 3430	. . 3 |- (E!xE.y e. A x = B <-> E.z {x | E.y e. A x = B } = {z })
2		eleq2 2098	. . . . . 6 |- ( {x | E.y e. A x = B } = {z } -> (x e. {x | E.y e. A x = B } <-> x e. {z }))
3		abid 2025	. . . . . 6 |- (x e. {x | E.y e. A x = B } <-> E.y e. A x = B)
4		elsn 3382	. . . . . 6 |- (x e. {z } <-> x = z)
5	2, 3, 4	3bitr3g 211	. . . . 5 |- ( {x | E.y e. A x = B } = {z } -> (E.y e. A x = B <-> x = z))
6		nfre1 2359	. . . . . . . . 9 |- F/yE.y e. A x = B
7	6	nfab 2179	. . . . . . . 8 |- F/_y {x | E.y e. A x = B }
8	7	nfeq1 2184	. . . . . . 7 |- F/y {x | E.y e. A x = B } = {z }
9		eusvobj1.1	. . . . . . . . 9 |- B e. _V
10	9	elabrex 5340	. . . . . . . 8 |- (y e. A -> B e. {x | E.y e. A x = B })
11		eleq2 2098	. . . . . . . . 9 |- ( {x | E.y e. A x = B } = {z } -> (B e. {x | E.y e. A x = B } <-> B e. {z }))
12	9	elsnc 3390	. . . . . . . . . 10 |- (B e. {z } <-> B = z)
13		eqcom 2039	. . . . . . . . . 10 |- (B = z <-> z = B)
14	12, 13	bitri 173	. . . . . . . . 9 |- (B e. {z } <-> z = B)
15	11, 14	syl6bb 185	. . . . . . . 8 |- ( {x | E.y e. A x = B } = {z } -> (B e. {x | E.y e. A x = B } <-> z = B))
16	10, 15	syl5ib 143	. . . . . . 7 |- ( {x | E.y e. A x = B } = {z } -> (y e. A -> z = B))
17	8, 16	ralrimi 2384	. . . . . 6 |- ( {x | E.y e. A x = B } = {z } -> A.y e. A z = B)
18		eqeq1 2043	. . . . . . 7 |- (x = z -> (x = B <-> z = B))
19	18	ralbidv 2320	. . . . . 6 |- (x = z -> (A.y e. A x = B <-> A.y e. A z = B))
20	17, 19	syl5ibrcom 146	. . . . 5 |- ( {x | E.y e. A x = B } = {z } -> (x = z -> A.y e. A x = B))
21	5, 20	sylbid 139	. . . 4 |- ( {x | E.y e. A x = B } = {z } -> (E.y e. A x = B -> A.y e. A x = B))
22	21	exlimiv 1486	. . 3 |- (E.z {x | E.y e. A x = B } = {z } -> (E.y e. A x = B -> A.y e. A x = B))
23	1, 22	sylbi 114	. 2 |- (E!xE.y e. A x = B -> (E.y e. A x = B -> A.y e. A x = B))
24		euex 1927	. . 3 |- (E!xE.y e. A x = B -> E.xE.y e. A x = B)
25		rexm 3314	. . . 4 |- (E.y e. A x = B -> E.y y e. A)
26	25	exlimiv 1486	. . 3 |- (E.xE.y e. A x = B -> E.y y e. A)
27		r19.2m 3303	. . . 4 |- ((E.y y e. A /\ A.y e. A x = B) -> E.y e. A x = B)
28	27	ex 108	. . 3 |- (E.y y e. A -> (A.y e. A x = B -> E.y e. A x = B))
29	24, 26, 28	3syl 17	. 2 |- (E!xE.y e. A x = B -> (A.y e. A x = B -> E.y e. A x = B))
30	23, 29	impbid 120	1 |- (E!xE.y e. A x = B -> (E.y e. A x = B <-> A.y e. A x = B))

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390  E!weu 1897   {cab 2023  A.wral 2300  E.wrex 2301   _Vcvv 2551   {csn 3367

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-sn 3373

This theorem is referenced by:  eusvobj1  5442