Theorem opelopabsb 4985

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 3203	. . . . . . . . . 10 |- x e. _V
2		vex 3203	. . . . . . . . . 10 |- y e. _V
3	1, 2	opnzi 4943	. . . . . . . . 9 |- <. x , y >. =/= (/)
4		simpl 473	. . . . . . . . . . 11 |- ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5	4	eqcomd 2628	. . . . . . . . . 10 |- ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6	5	necon3ai 2819	. . . . . . . . 9 |- ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7	3, 6	ax-mp 5	. . . . . . . 8 |- -. ( (/) = <. x , y >. /\ ph )
8	7	nex 1731	. . . . . . 7 |- -. E. y ( (/) = <. x , y >. /\ ph )
9	8	nex 1731	. . . . . 6 |- -. E. x E. y ( (/) = <. x , y >. /\ ph )
10		elopab 4983	. . . . . 6 |- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11	9, 10	mtbir 313	. . . . 5 |- -. (/) e. { <. x , y >. | ph }
12		eleq1 2689	. . . . 5 |- ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13	11, 12	mtbiri 317	. . . 4 |- ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14	13	necon2ai 2823	. . 3 |- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15		opnz 4942	. . 3 |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
16	14, 15	sylib 208	. 2 |- ( <. A , B >. e. { <. x , y >. | ph } -> ( A e. _V /\ B e. _V ) )
17		sbcex 3445	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18		spesbc 3521	. . . 4 |- ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19		sbcex 3445	. . . . 5 |- ( [. B / y ]. ph -> B e. _V )
20	19	exlimiv 1858	. . . 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 554	. 2 |- ( [. A / x ]. [. B / y ]. ph -> ( A e. _V /\ B e. _V ) )
23		opeq1 4402	. . . . 5 |- ( z = A -> <. z , w >. = <. A , w >. )
24	23	eleq1d 2686	. . . 4 |- ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25		dfsbcq2 3438	. . . 4 |- ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26	24, 25	bibi12d 335	. . 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 4403	. . . . 5 |- ( w = B -> <. A , w >. = <. A , B >. )
28	27	eleq1d 2686	. . . 4 |- ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29		dfsbcq2 3438	. . . . 5 |- ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30	29	sbcbidv 3490	. . . 4 |- ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31	28, 30	bibi12d 335	. . 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 4719	. . . . . 6 |- F/_ x { <. x , y >. | ph }
33	32	nfel2 2781	. . . . 5 |- F/ x <. z , w >. e. { <. x , y >. | ph }
34		nfs1v 2437	. . . . 5 |- F/ x [ z / x ] [ w / y ] ph
35	33, 34	nfbi 1833	. . . 4 |- F/ x ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
36		opeq1 4402	. . . . . 6 |- ( x = z -> <. x , w >. = <. z , w >. )
37	36	eleq1d 2686	. . . . 5 |- ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38		sbequ12 2111	. . . . 5 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39	37, 38	bibi12d 335	. . . 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 4720	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
41	40	nfel2 2781	. . . . . 6 |- F/ y <. x , w >. e. { <. x , y >. | ph }
42		nfs1v 2437	. . . . . 6 |- F/ y [ w / y ] ph
43	41, 42	nfbi 1833	. . . . 5 |- F/ y ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
44		opeq2 4403	. . . . . . 7 |- ( y = w -> <. x , y >. = <. x , w >. )
45	44	eleq1d 2686	. . . . . 6 |- ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46		sbequ12 2111	. . . . . 6 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
47	45, 46	bibi12d 335	. . . . 5 |- ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48		opabid 4982	. . . . 5 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49	43, 47, 48	chvar 2262	. . . 4 |- ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50	35, 39, 49	chvar 2262	. . 3 |- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51	26, 31, 50	vtocl2g 3270	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52	16, 22, 51	pm5.21nii 368	1 |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   [wsb 1880   e. wcel 1990   =/= wne 2794   _Vcvv 3200   [.wsbc 3435   (/)c0 3915   <.cop 4183   {copab 4712

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-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  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-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-opab 4713

This theorem is referenced by:  brabsb  4986  opelopabgf  4995  opelopabaf  4999  opelopabf  5000  difopab  5253  isarep1  5977  fmptsnd  6435