Theorem sbcel12g 2007

Description: Distribute proper substitution through a membership relation.

Assertion

Ref	Expression
sbcel12g	⊢ (A ∈ D → ([A / x]B ∈ C ↔ [A / x]B ∈ [A / x]C))

Proof of Theorem sbcel12g

Step	Hyp	Ref	Expression
1		elisset 1813	. . 3 ⊢ (A ∈ D → A ∈ V)
2		sbcexg 1971	. . . . 5 ⊢ (A ∈ V → ([A / x]∃z(z = B ⋀ z ∈ C) ↔ ∃z[A / x](z = B ⋀ z ∈ C)))
3		df-clel 1470	. . . . . 6 ⊢ (B ∈ C ↔ ∃z(z = B ⋀ z ∈ C))
4	3	sbcbii 1974	. . . . 5 ⊢ (A ∈ V → ([A / x]B ∈ C ↔ [A / x]∃z(z = B ⋀ z ∈ C)))
5		dfcleq 1468	. . . . . . . . . . 11 ⊢ (z = B ↔ ∀y(y ∈ z ↔ y ∈ B))
6	5	sbcbii 1974	. . . . . . . . . 10 ⊢ (A ∈ V → ([A / x]z = B ↔ [A / x]∀y(y ∈ z ↔ y ∈ B)))
7		sbcalg 1970	. . . . . . . . . 10 ⊢ (A ∈ V → ([A / x]∀y(y ∈ z ↔ y ∈ B) ↔ ∀y[A / x](y ∈ z ↔ y ∈ B)))
8		sbcbidig 1969	. . . . . . . . . . . 12 ⊢ (A ∈ V → ([A / x](y ∈ z ↔ y ∈ B) ↔ ([A / x]y ∈ z ↔ [A / x]y ∈ B)))
9		ax-17 969	. . . . . . . . . . . . . 14 ⊢ (y ∈ z → ∀x y ∈ z)
10	9	sbcgf 1982	. . . . . . . . . . . . 13 ⊢ (A ∈ V → ([A / x]y ∈ z ↔ y ∈ z))
11	10	bibi1d 618	. . . . . . . . . . . 12 ⊢ (A ∈ V → (([A / x]y ∈ z ↔ [A / x]y ∈ B) ↔ (y ∈ z ↔ [A / x]y ∈ B)))
12	8, 11	bitrd 527	. . . . . . . . . . 11 ⊢ (A ∈ V → ([A / x](y ∈ z ↔ y ∈ B) ↔ (y ∈ z ↔ [A / x]y ∈ B)))
13	12	albidv 1276	. . . . . . . . . 10 ⊢ (A ∈ V → (∀y[A / x](y ∈ z ↔ y ∈ B) ↔ ∀y(y ∈ z ↔ [A / x]y ∈ B)))
14	6, 7, 13	3bitrd 543	. . . . . . . . 9 ⊢ (A ∈ V → ([A / x]z = B ↔ ∀y(y ∈ z ↔ [A / x]y ∈ B)))
15		abeq2 1565	. . . . . . . . 9 ⊢ (z = {y∣[A / x]y ∈ B} ↔ ∀y(y ∈ z ↔ [A / x]y ∈ B))
16	14, 15	syl6rbbr 538	. . . . . . . 8 ⊢ (A ∈ V → (z = {y∣[A / x]y ∈ B} ↔ [A / x]z = B))
17		eleq1 1531	. . . . . . . . . . . 12 ⊢ (y = z → (y ∈ C ↔ z ∈ C))
18	17	sbcbidv 1973	. . . . . . . . . . 11 ⊢ ((y = z ⋀ A ∈ V) → ([A / x]y ∈ C ↔ [A / x]z ∈ C))
19	18	expcom 374	. . . . . . . . . 10 ⊢ (A ∈ V → (y = z → ([A / x]y ∈ C ↔ [A / x]z ∈ C)))
20	19	19.21aiv 1284	. . . . . . . . 9 ⊢ (A ∈ V → ∀y(y = z → ([A / x]y ∈ C ↔ [A / x]z ∈ C)))
21		visset 1809	. . . . . . . . . 10 ⊢ z ∈ V
22		elabgt 1891	. . . . . . . . . 10 ⊢ ((z ∈ V ⋀ ∀y(y = z → ([A / x]y ∈ C ↔ [A / x]z ∈ C))) → (z ∈ {y∣[A / x]y ∈ C} ↔ [A / x]z ∈ C))
23	21, 22	mpan 694	. . . . . . . . 9 ⊢ (∀y(y = z → ([A / x]y ∈ C ↔ [A / x]z ∈ C)) → (z ∈ {y∣[A / x]y ∈ C} ↔ [A / x]z ∈ C))
24	20, 23	syl 10	. . . . . . . 8 ⊢ (A ∈ V → (z ∈ {y∣[A / x]y ∈ C} ↔ [A / x]z ∈ C))
25	16, 24	anbi12d 627	. . . . . . 7 ⊢ (A ∈ V → ((z = {y∣[A / x]y ∈ B} ⋀ z ∈ {y∣[A / x]y ∈ C}) ↔ ([A / x]z = B ⋀ [A / x]z ∈ C)))
26		sbcang 1967	. . . . . . 7 ⊢ (A ∈ V → ([A / x](z = B ⋀ z ∈ C) ↔ ([A / x]z = B ⋀ [A / x]z ∈ C)))
27	25, 26	bitr4d 530	. . . . . 6 ⊢ (A ∈ V → ((z = {y∣[A / x]y ∈ B} ⋀ z ∈ {y∣[A / x]y ∈ C}) ↔ [A / x](z = B ⋀ z ∈ C)))
28	27	exbidv 1277	. . . . 5 ⊢ (A ∈ V → (∃z(z = {y∣[A / x]y ∈ B} ⋀ z ∈ {y∣[A / x]y ∈ C}) ↔ ∃z[A / x](z = B ⋀ z ∈ C)))
29	2, 4, 28	3bitr4d 549	. . . 4 ⊢ (A ∈ V → ([A / x]B ∈ C ↔ ∃z(z = {y∣[A / x]y ∈ B} ⋀ z ∈ {y∣[A / x]y ∈ C})))
30		df-clel 1470	. . . 4 ⊢ ({y∣[A / x]y ∈ B} ∈ {y∣[A / x]y ∈ C} ↔ ∃z(z = {y∣[A / x]y ∈ B} ⋀ z ∈ {y∣[A / x]y ∈ C}))
31	29, 30	syl6bbr 537	. . 3 ⊢ (A ∈ V → ([A / x]B ∈ C ↔ {y∣[A / x]y ∈ B} ∈ {y∣[A / x]y ∈ C}))
32	1, 31	syl 10	. 2 ⊢ (A ∈ D → ([A / x]B ∈ C ↔ {y∣[A / x]y ∈ B} ∈ {y∣[A / x]y ∈ C}))
33		df-csb 1998	. . 3 ⊢ [A / x]B = {y∣[A / x]y ∈ B}
34		df-csb 1998	. . 3 ⊢ [A / x]C = {y∣[A / x]y ∈ C}
35	33, 34	eleq12i 1536	. 2 ⊢ ([A / x]B ∈ [A / x]C ↔ {y∣[A / x]y ∈ B} ∈ {y∣[A / x]y ∈ C})
36	32, 35	syl6bbr 537	1 ⊢ (A ∈ D → ([A / x]B ∈ C ↔ [A / x]B ∈ [A / x]C))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  {cab 1461  Vcvv 1807  [csb 1997

This theorem is referenced by:  sbcel1g 2009  sbcel2g 2011  sbccsb2g 2019  sbcnestg 2034

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-sbc 1938  df-csb 1998

Copyright terms: Public domain