Theorem opelopabsb 4757

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 3116	. . . . . . . . . 10 |- x e. _V
2		vex 3116	. . . . . . . . . 10 |- y e. _V
3	1, 2	opnzi 4719	. . . . . . . . 9 |- <. x , y >. =/= (/)
4		simpl 457	. . . . . . . . . . 11 |- ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5	4	eqcomd 2475	. . . . . . . . . 10 |- ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6	5	necon3ai 2695	. . . . . . . . 9 |- ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7	3, 6	ax-mp 5	. . . . . . . 8 |- -. ( (/) = <. x , y >. /\ ph )
8	7	nex 1610	. . . . . . 7 |- -. E. y ( (/) = <. x , y >. /\ ph )
9	8	nex 1610	. . . . . 6 |- -. E. x E. y ( (/) = <. x , y >. /\ ph )
10		elopab 4755	. . . . . 6 |- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11	9, 10	mtbir 299	. . . . 5 |- -. (/) e. { <. x , y >. | ph }
12		eleq1 2539	. . . . 5 |- ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13	11, 12	mtbiri 303	. . . 4 |- ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14	13	necon2ai 2702	. . 3 |- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15		opnz 4718	. . 3 |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
16	14, 15	sylib 196	. 2 |- ( <. A , B >. e. { <. x , y >. | ph } -> ( A e. _V /\ B e. _V ) )
17		sbcex 3341	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18		spesbc 3424	. . . 4 |- ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19		sbcex 3341	. . . . 5 |- ( [. B / y ]. ph -> B e. _V )
20	19	exlimiv 1698	. . . 4 |- ( E. x [. B / y ]. ph -> B e. _V )
21	18, 20	syl 16	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> B e. _V )
22	17, 21	jca 532	. 2 |- ( [. A / x ]. [. B / y ]. ph -> ( A e. _V /\ B e. _V ) )
23		opeq1 4213	. . . . 5 |- ( z = A -> <. z , w >. = <. A , w >. )
24	23	eleq1d 2536	. . . 4 |- ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25		dfsbcq2 3334	. . . 4 |- ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26	24, 25	bibi12d 321	. . 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 4214	. . . . 5 |- ( w = B -> <. A , w >. = <. A , B >. )
28	27	eleq1d 2536	. . . 4 |- ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29		dfsbcq2 3334	. . . . 5 |- ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30	29	sbcbidv 3390	. . . 4 |- ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31	28, 30	bibi12d 321	. . 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 4513	. . . . . 6 |- F/_ x { <. x , y >. | ph }
33	32	nfel2 2647	. . . . 5 |- F/ x <. z , w >. e. { <. x , y >. | ph }
34		nfs1v 2164	. . . . 5 |- F/ x [ z / x ] [ w / y ] ph
35	33, 34	nfbi 1881	. . . 4 |- F/ x ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
36		opeq1 4213	. . . . . 6 |- ( x = z -> <. x , w >. = <. z , w >. )
37	36	eleq1d 2536	. . . . 5 |- ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38		sbequ12 1961	. . . . 5 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39	37, 38	bibi12d 321	. . . 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 4514	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
41	40	nfel2 2647	. . . . . 6 |- F/ y <. x , w >. e. { <. x , y >. | ph }
42		nfs1v 2164	. . . . . 6 |- F/ y [ w / y ] ph
43	41, 42	nfbi 1881	. . . . 5 |- F/ y ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
44		opeq2 4214	. . . . . . 7 |- ( y = w -> <. x , y >. = <. x , w >. )
45	44	eleq1d 2536	. . . . . 6 |- ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46		sbequ12 1961	. . . . . 6 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
47	45, 46	bibi12d 321	. . . . 5 |- ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48		opabid 4754	. . . . 5 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49	43, 47, 48	chvar 1982	. . . 4 |- ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50	35, 39, 49	chvar 1982	. . 3 |- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51	26, 31, 50	vtocl2g 3175	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52	16, 22, 51	pm5.21nii 353	1 |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 369   = wceq 1379   E.wex 1596   [wsb 1711   e. wcel 1767   =/= wne 2662   _Vcvv 3113   [.wsbc 3331   (/)c0 3785   <.cop 4033   {copab 4504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506

This theorem is referenced by:  brabsb  4758  opelopabgf  4767  opelopabaf  4771  opelopabf  4772  difopab  5132  isarep1  5665  fmptsnd  6081