Theorem opelopabsb 4699

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 3061	. . . . . . . . . 10 |- x e. _V
2		vex 3061	. . . . . . . . . 10 |- y e. _V
3	1, 2	opnzi 4662	. . . . . . . . 9 |- <. x , y >. =/= (/)
4		simpl 455	. . . . . . . . . . 11 |- ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5	4	eqcomd 2410	. . . . . . . . . 10 |- ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6	5	necon3ai 2631	. . . . . . . . 9 |- ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7	3, 6	ax-mp 5	. . . . . . . 8 |- -. ( (/) = <. x , y >. /\ ph )
8	7	nex 1648	. . . . . . 7 |- -. E. y ( (/) = <. x , y >. /\ ph )
9	8	nex 1648	. . . . . 6 |- -. E. x E. y ( (/) = <. x , y >. /\ ph )
10		elopab 4697	. . . . . 6 |- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11	9, 10	mtbir 297	. . . . 5 |- -. (/) e. { <. x , y >. | ph }
12		eleq1 2474	. . . . 5 |- ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13	11, 12	mtbiri 301	. . . 4 |- ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14	13	necon2ai 2638	. . 3 |- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15		opnz 4661	. . 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 3286	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18		spesbc 3358	. . . 4 |- ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19		sbcex 3286	. . . . 5 |- ( [. B / y ]. ph -> B e. _V )
20	19	exlimiv 1743	. . . 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 530	. 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 2471	. . . 4 |- ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25		dfsbcq2 3279	. . . 4 |- ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26	24, 25	bibi12d 319	. . 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 2471	. . . 4 |- ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29		dfsbcq2 3279	. . . . 5 |- ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30	29	sbcbidv 3331	. . . 4 |- ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31	28, 30	bibi12d 319	. . 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 4460	. . . . . 6 |- F/_ x { <. x , y >. | ph }
33	32	nfel2 2582	. . . . 5 |- F/ x <. z , w >. e. { <. x , y >. | ph }
34		nfs1v 2205	. . . . 5 |- F/ x [ z / x ] [ w / y ] ph
35	33, 34	nfbi 1962	. . . 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 2471	. . . . 5 |- ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38		sbequ12 2020	. . . . 5 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39	37, 38	bibi12d 319	. . . 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 4461	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
41	40	nfel2 2582	. . . . . 6 |- F/ y <. x , w >. e. { <. x , y >. | ph }
42		nfs1v 2205	. . . . . 6 |- F/ y [ w / y ] ph
43	41, 42	nfbi 1962	. . . . 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 2471	. . . . . 6 |- ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46		sbequ12 2020	. . . . . 6 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
47	45, 46	bibi12d 319	. . . . 5 |- ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48		opabid 4696	. . . . 5 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49	43, 47, 48	chvar 2040	. . . 4 |- ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50	35, 39, 49	chvar 2040	. . 3 |- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51	26, 31, 50	vtocl2g 3120	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52	16, 22, 51	pm5.21nii 351	1 |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 367   = wceq 1405   E.wex 1633   [wsb 1763   e. wcel 1842   =/= wne 2598   _Vcvv 3058   [.wsbc 3276   (/)c0 3737   <.cop 3977   {copab 4451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453

This theorem is referenced by:  brabsb  4700  opelopabgf  4709  opelopabaf  4713  opelopabf  4714  difopab  4954  isarep1  5647  fmptsnd  6072