Theorem opelopabsb 4730

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 3083	. . . . . . . . . 10 |- x e. _V
2		vex 3083	. . . . . . . . . 10 |- y e. _V
3	1, 2	opnzi 4693	. . . . . . . . 9 |- <. x , y >. =/= (/)
4		simpl 458	. . . . . . . . . . 11 |- ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5	4	eqcomd 2430	. . . . . . . . . 10 |- ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6	5	necon3ai 2648	. . . . . . . . 9 |- ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7	3, 6	ax-mp 5	. . . . . . . 8 |- -. ( (/) = <. x , y >. /\ ph )
8	7	nex 1672	. . . . . . 7 |- -. E. y ( (/) = <. x , y >. /\ ph )
9	8	nex 1672	. . . . . 6 |- -. E. x E. y ( (/) = <. x , y >. /\ ph )
10		elopab 4728	. . . . . 6 |- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11	9, 10	mtbir 300	. . . . 5 |- -. (/) e. { <. x , y >. | ph }
12		eleq1 2495	. . . . 5 |- ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13	11, 12	mtbiri 304	. . . 4 |- ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14	13	necon2ai 2655	. . 3 |- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15		opnz 4692	. . 3 |- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
16	14, 15	sylib 199	. 2 |- ( <. A , B >. e. { <. x , y >. | ph } -> ( A e. _V /\ B e. _V ) )
17		sbcex 3309	. . 3 |- ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18		spesbc 3381	. . . 4 |- ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19		sbcex 3309	. . . . 5 |- ( [. B / y ]. ph -> B e. _V )
20	19	exlimiv 1770	. . . 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 534	. 2 |- ( [. A / x ]. [. B / y ]. ph -> ( A e. _V /\ B e. _V ) )
23		opeq1 4187	. . . . 5 |- ( z = A -> <. z , w >. = <. A , w >. )
24	23	eleq1d 2491	. . . 4 |- ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25		dfsbcq2 3302	. . . 4 |- ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26	24, 25	bibi12d 322	. . 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 4188	. . . . 5 |- ( w = B -> <. A , w >. = <. A , B >. )
28	27	eleq1d 2491	. . . 4 |- ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29		dfsbcq2 3302	. . . . 5 |- ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30	29	sbcbidv 3354	. . . 4 |- ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31	28, 30	bibi12d 322	. . 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 4490	. . . . . 6 |- F/_ x { <. x , y >. | ph }
33	32	nfel2 2598	. . . . 5 |- F/ x <. z , w >. e. { <. x , y >. | ph }
34		nfs1v 2236	. . . . 5 |- F/ x [ z / x ] [ w / y ] ph
35	33, 34	nfbi 1994	. . . 4 |- F/ x ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
36		opeq1 4187	. . . . . 6 |- ( x = z -> <. x , w >. = <. z , w >. )
37	36	eleq1d 2491	. . . . 5 |- ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38		sbequ12 2051	. . . . 5 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39	37, 38	bibi12d 322	. . . 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 4491	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
41	40	nfel2 2598	. . . . . 6 |- F/ y <. x , w >. e. { <. x , y >. | ph }
42		nfs1v 2236	. . . . . 6 |- F/ y [ w / y ] ph
43	41, 42	nfbi 1994	. . . . 5 |- F/ y ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
44		opeq2 4188	. . . . . . 7 |- ( y = w -> <. x , y >. = <. x , w >. )
45	44	eleq1d 2491	. . . . . 6 |- ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46		sbequ12 2051	. . . . . 6 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
47	45, 46	bibi12d 322	. . . . 5 |- ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48		opabid 4727	. . . . 5 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49	43, 47, 48	chvar 2071	. . . 4 |- ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50	35, 39, 49	chvar 2071	. . 3 |- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51	26, 31, 50	vtocl2g 3143	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52	16, 22, 51	pm5.21nii 354	1 |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Syntax hints:   -. wn 3   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1657   [wsb 1790   e. wcel 1872   =/= wne 2614   _Vcvv 3080   [.wsbc 3299   (/)c0 3761   <.cop 4004   {copab 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-opab 4483

This theorem is referenced by:  brabsb  4731  opelopabgf  4740  opelopabaf  4744  opelopabf  4745  difopab  4985  isarep1  5680  fmptsnd  6101