Theorem opelopabsb 4711

Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)

Assertion

Ref	Expression
opelopabsb	|- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Distinct variable groups:   x, y   x, B

Allowed substitution hints:   ph( x, y)   A( x, y)   B( y)

Proof of Theorem opelopabsb

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3034	. . . . . . . . . 10 |- x e. _V
2		vex 3034	. . . . . . . . . 10 |- y e. _V
3	1, 2	opnzi 4674	. . . . . . . . 9 |- <. x , y >. =/= (/)
4		simpl 464	. . . . . . . . . . 11 |- ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5	4	eqcomd 2477	. . . . . . . . . 10 |- ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6	5	necon3ai 2668	. . . . . . . . 9 |- ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7	3, 6	ax-mp 5	. . . . . . . 8 |- -. ( (/) = <. x , y >. /\ ph )
8	7	nex 1686	. . . . . . 7 |- -. E. y ( (/) = <. x , y >. /\ ph )
9	8	nex 1686	. . . . . 6 |- -. E. x E. y ( (/) = <. x , y >. /\ ph )
10		elopab 4709	. . . . . 6 |- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11	9, 10	mtbir 306	. . . . 5 |- -. (/) e. { <. x , y >. | ph }
12		eleq1 2537	. . . . 5 |- ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13	11, 12	mtbiri 310	. . . 4 |- ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14	13	necon2ai 2672	. . 3 |- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15		opnz 4673	. . 3 |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
16	14, 15	sylib 201	. 2 |- ( <. A , B >. e. { <. x , y >. | ph } -> ( A e. _V /\ B e. _V ) )
17		sbcex 3265	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18		spesbc 3337	. . . 4 |- ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19		sbcex 3265	. . . . 5 |- ( [. B / y ]. ph -> B e. _V )
20	19	exlimiv 1784	. . . 4 |- ( E. x [. B / y ]. ph -> B e. _V )
21	18, 20	syl 17	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> B e. _V )
22	17, 21	jca 541	. 2 |- ( [. A / x ]. [. B / y ]. ph -> ( A e. _V /\ B e. _V ) )
23		opeq1 4158	. . . . 5 |- ( z = A -> <. z , w >. = <. A , w >. )
24	23	eleq1d 2533	. . . 4 |- ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25		dfsbcq2 3258	. . . 4 |- ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26	24, 25	bibi12d 328	. . 3 |- ( z = A -> ( ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph ) <-> ( <. A , w >. e. { <. x , y >. | ph } <-> [. A / x ]. [ w / y ] ph ) ) )
27		opeq2 4159	. . . . 5 |- ( w = B -> <. A , w >. = <. A , B >. )
28	27	eleq1d 2533	. . . 4 |- ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29		dfsbcq2 3258	. . . . 5 |- ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30	29	sbcbidv 3310	. . . 4 |- ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31	28, 30	bibi12d 328	. . 3 |- ( w = B -> ( ( <. A , w >. e. { <. x , y >. | ph } <-> [. A / x ]. [ w / y ] ph ) <-> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) ) )
32		nfopab1 4462	. . . . . 6 |- F/_ x { <. x , y >. | ph }
33	32	nfel2 2628	. . . . 5 |- F/ x <. z , w >. e. { <. x , y >. | ph }
34		nfs1v 2286	. . . . 5 |- F/ x [ z / x ] [ w / y ] ph
35	33, 34	nfbi 2037	. . . 4 |- F/ x ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
36		opeq1 4158	. . . . . 6 |- ( x = z -> <. x , w >. = <. z , w >. )
37	36	eleq1d 2533	. . . . 5 |- ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38		sbequ12 2098	. . . . 5 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39	37, 38	bibi12d 328	. . . 4 |- ( x = z -> ( ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) <-> ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph ) ) )
40		nfopab2 4463	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
41	40	nfel2 2628	. . . . . 6 |- F/ y <. x , w >. e. { <. x , y >. | ph }
42		nfs1v 2286	. . . . . 6 |- F/ y [ w / y ] ph
43	41, 42	nfbi 2037	. . . . 5 |- F/ y ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
44		opeq2 4159	. . . . . . 7 |- ( y = w -> <. x , y >. = <. x , w >. )
45	44	eleq1d 2533	. . . . . 6 |- ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46		sbequ12 2098	. . . . . 6 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
47	45, 46	bibi12d 328	. . . . 5 |- ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48		opabid 4708	. . . . 5 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49	43, 47, 48	chvar 2119	. . . 4 |- ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50	35, 39, 49	chvar 2119	. . 3 |- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51	26, 31, 50	vtocl2g 3097	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52	16, 22, 51	pm5.21nii 360	1 |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Syntax hints:   -. wn 3   <-> wb 189   /\ wa 376   = wceq 1452   E.wex 1671   [wsb 1805   e. wcel 1904   =/= wne 2641   _Vcvv 3031   [.wsbc 3255   (/)c0 3722   <.cop 3965   {copab 4453

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-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-opab 4455

This theorem is referenced by:  brabsb  4712  opelopabgf  4721  opelopabaf  4725  opelopabf  4726  difopab  4971  isarep1  5672  fmptsnd  6102