Theorem bnj1310 13979

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj1310.1	|- (ch -> E.x e. B ph)
bnj1310.2	|- (th <-> (ch /\ x e. B /\ ph))
bnj1310.3	|- (ch -> A.xch)
bnj1310.4	|- (w e. B -> A.x w e. B)

Assertion

Ref	Expression
bnj1310	|- (ch -> E.xth)

Distinct variable groups:   w,B   x,w

Proof of Theorem bnj1310

Step	Hyp	Ref	Expression
1		bnj1310.1	. . . 4 |- (ch -> E.x e. B ph)
2		ax-17 1634	. . . . . . 7 |- ((ch -> (x e. B /\ ph)) -> A.y(ch -> (x e. B /\ ph)))
3		bnj1310.3	. . . . . . . 8 |- (ch -> A.xch)
4		bnj1310.4	. . . . . . . . . 10 |- (w e. B -> A.x w e. B)
5	4	hblem 2273	. . . . . . . . 9 |- (y e. B -> A.x y e. B)
6		hbs1 2014	. . . . . . . . 9 |- ([y / x]ph -> A.x[y / x]ph)
7	5, 6	hban 1674	. . . . . . . 8 |- ((y e. B /\ [y / x]ph) -> A.x(y e. B /\ [y / x]ph))
8	3, 7	hbim 1672	. . . . . . 7 |- ((ch -> (y e. B /\ [y / x]ph)) -> A.x(ch -> (y e. B /\ [y / x]ph)))
9		eleq1 2233	. . . . . . . . 9 |- (x = y -> (x e. B <-> y e. B))
10		sbequ12 1854	. . . . . . . . 9 |- (x = y -> (ph <-> [y / x]ph))
11	9, 10	anbi12d 821	. . . . . . . 8 |- (x = y -> ((x e. B /\ ph) <-> (y e. B /\ [y / x]ph)))
12	11	imbi2d 380	. . . . . . 7 |- (x = y -> ((ch -> (x e. B /\ ph)) <-> (ch -> (y e. B /\ [y / x]ph))))
13	2, 8, 12	cbvex 1838	. . . . . 6 |- (E.x(ch -> (x e. B /\ ph)) <-> E.y(ch -> (y e. B /\ [y / x]ph)))
14	3	19.37 1746	. . . . . 6 |- (E.x(ch -> (x e. B /\ ph)) <-> (ch -> E.x(x e. B /\ ph)))
15		19.37v 1980	. . . . . 6 |- (E.y(ch -> (y e. B /\ [y / x]ph)) <-> (ch -> E.y(y e. B /\ [y / x]ph)))
16	13, 14, 15	3bitr3i 338	. . . . 5 |- ((ch -> E.x(x e. B /\ ph)) <-> (ch -> E.y(y e. B /\ [y / x]ph)))
17		df-rex 2390	. . . . . 6 |- (E.x e. B ph <-> E.x(x e. B /\ ph))
18	17	imbi2i 373	. . . . 5 |- ((ch -> E.x e. B ph) <-> (ch -> E.x(x e. B /\ ph)))
19		df-rex 2390	. . . . . 6 |- (E.y e. B [y / x]ph <-> E.y(y e. B /\ [y / x]ph))
20	19	imbi2i 373	. . . . 5 |- ((ch -> E.y e. B [y / x]ph) <-> (ch -> E.y(y e. B /\ [y / x]ph)))
21	16, 18, 20	3bitr4i 340	. . . 4 |- ((ch -> E.x e. B ph) <-> (ch -> E.y e. B [y / x]ph))
22	1, 21	mpbi 254	. . 3 |- (ch -> E.y e. B [y / x]ph)
23		hbs1 2014	. . . . 5 |- ([y / x]th -> A.x[y / x]th)
24	3, 5, 6	hb3an 1677	. . . . 5 |- ((ch /\ y e. B /\ [y / x]ph) -> A.x(ch /\ y e. B /\ [y / x]ph))
25	23, 24	hbbi 1675	. . . 4 |- (([y / x]th <-> (ch /\ y e. B /\ [y / x]ph)) -> A.x([y / x]th <-> (ch /\ y e. B /\ [y / x]ph)))
26		sbequ12 1854	. . . . 5 |- (x = y -> (th <-> [y / x]th))
27	9, 10	3anbi23d 1472	. . . . 5 |- (x = y -> ((ch /\ x e. B /\ ph) <-> (ch /\ y e. B /\ [y / x]ph)))
28	26, 27	bibi12d 385	. . . 4 |- (x = y -> ((th <-> (ch /\ x e. B /\ ph)) <-> ([y / x]th <-> (ch /\ y e. B /\ [y / x]ph))))
29		bnj1310.2	. . . 4 |- (th <-> (ch /\ x e. B /\ ph))
30	25, 28, 29	chvar 1839	. . 3 |- ([y / x]th <-> (ch /\ y e. B /\ [y / x]ph))
31	22, 30	bnj1209 13912	. 2 |- (ch -> E.y[y / x]th)
32		ax-17 1634	. . 3 |- (th -> A.yth)
33	32	sb8e 1938	. 2 |- (E.xth <-> E.y[y / x]th)
34	31, 33	sylibr 264	1 |- (ch -> E.xth)

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130  A.wal 1613   = wceq 1615   e. wcel 1617  E.wex 1644  [wsbc 1843  E.wrex 2386

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-cleq 2163  df-clel 2166  df-rex 2390

Copyright terms: Public domain