Theorem iunopeqop 4981

Description: Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.)

Hypotheses

Ref	Expression
iunopeqop.b	|- B e. _V
iunopeqop.c	|- C e. _V
iunopeqop.d	|- D e. _V

Assertion

Ref	Expression
iunopeqop	|- ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )

Distinct variable groups:   x, A, z   x, C   x, D

Allowed substitution hints:   B( x, z)   C( z)   D( z)

Proof of Theorem iunopeqop

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0snor2el 4364	. 2 |- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
2		nfiu1 4550	. . . . . 6 |- F/_ x U_ x e. A { <. x , B >. }
3	2	nfeq1 2778	. . . . 5 |- F/ x U_ x e. A { <. x , B >. } = <. C , D >.
4		nfv 1843	. . . . 5 |- F/ x E. z A = { z }
5	3, 4	nfim 1825	. . . 4 |- F/ x ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } )
6		ssiun2 4563	. . . . . . 7 |- ( x e. A -> { <. x , B >. } C_ U_ x e. A { <. x , B >. } )
7		nfcv 2764	. . . . . . . 8 |- F/_ x y
8		nfcsb1v 3549	. . . . . . . . . . 11 |- F/_ x [_ y / x ]_ B
9	7, 8	nfop 4418	. . . . . . . . . 10 |- F/_ x <. y , [_ y / x ]_ B >.
10	9	nfsn 4242	. . . . . . . . 9 |- F/_ x { <. y , [_ y / x ]_ B >. }
11	10, 2	nfss 3596	. . . . . . . 8 |- F/ x { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. }
12		id 22	. . . . . . . . . . 11 |- ( x = y -> x = y )
13		csbeq1a 3542	. . . . . . . . . . 11 |- ( x = y -> B = [_ y / x ]_ B )
14	12, 13	opeq12d 4410	. . . . . . . . . 10 |- ( x = y -> <. x , B >. = <. y , [_ y / x ]_ B >. )
15	14	sneqd 4189	. . . . . . . . 9 |- ( x = y -> { <. x , B >. } = { <. y , [_ y / x ]_ B >. } )
16	15	sseq1d 3632	. . . . . . . 8 |- ( x = y -> ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } <-> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) )
17	7, 11, 16, 6	vtoclgaf 3271	. . . . . . 7 |- ( y e. A -> { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } )
18	6, 17	anim12i 590	. . . . . 6 |- ( ( x e. A /\ y e. A ) -> ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) )
19		unss 3787	. . . . . . 7 |- ( ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) <-> ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } )
20		sseq2 3627	. . . . . . . . 9 |- ( U_ x e. A { <. x , B >. } = <. C , D >. -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } <-> ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. ) )
21		df-pr 4180	. . . . . . . . . . . 12 |- { <. x , B >. , <. y , [_ y / x ]_ B >. } = ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } )
22	21	eqcomi 2631	. . . . . . . . . . 11 |- ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) = { <. x , B >. , <. y , [_ y / x ]_ B >. }
23	22	sseq1i 3629	. . . . . . . . . 10 |- ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. <-> { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. )
24		vex 3203	. . . . . . . . . . . 12 |- x e. _V
25		iunopeqop.b	. . . . . . . . . . . 12 |- B e. _V
26		vex 3203	. . . . . . . . . . . 12 |- y e. _V
27	25	csbex 4793	. . . . . . . . . . . 12 |- [_ y / x ]_ B e. _V
28		iunopeqop.c	. . . . . . . . . . . 12 |- C e. _V
29		iunopeqop.d	. . . . . . . . . . . 12 |- D e. _V
30	24, 25, 26, 27, 28, 29	propssopi 4971	. . . . . . . . . . 11 |- ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> x = y )
31		eqneqall 2805	. . . . . . . . . . 11 |- ( x = y -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
32	30, 31	syl 17	. . . . . . . . . 10 |- ( { <. x , B >. , <. y , [_ y / x ]_ B >. } C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
33	23, 32	sylbi 207	. . . . . . . . 9 |- ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ <. C , D >. -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) )
34	20, 33	syl6bi 243	. . . . . . . 8 |- ( U_ x e. A { <. x , B >. } = <. C , D >. -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } -> ( x =/= y -> ( ( x e. A /\ y e. A ) -> E. z A = { z } ) ) ) )
35	34	com14 96	. . . . . . 7 |- ( ( x e. A /\ y e. A ) -> ( ( { <. x , B >. } u. { <. y , [_ y / x ]_ B >. } ) C_ U_ x e. A { <. x , B >. } -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) ) )
36	19, 35	syl5bi 232	. . . . . 6 |- ( ( x e. A /\ y e. A ) -> ( ( { <. x , B >. } C_ U_ x e. A { <. x , B >. } /\ { <. y , [_ y / x ]_ B >. } C_ U_ x e. A { <. x , B >. } ) -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) ) )
37	18, 36	mpd 15	. . . . 5 |- ( ( x e. A /\ y e. A ) -> ( x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
38	37	rexlimdva 3031	. . . 4 |- ( x e. A -> ( E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) ) )
39	5, 38	rexlimi 3024	. . 3 |- ( E. x e. A E. y e. A x =/= y -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
40		ax-1 6	. . 3 |- ( E. z A = { z } -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
41	39, 40	jaoi 394	. 2 |- ( ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
42	1, 41	syl 17	1 |- ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   [_csb 3533   u. cun 3572   C_ wss 3574   (/)c0 3915   {csn 4177   {cpr 4179   <.cop 4183   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-iun 4522

This theorem is referenced by:  funopsn  6413