Theorem sbcbrg 2658

Description: Move substitution in and out of a binary relation.

Assertion

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

Proof of Theorem sbcbrg

Step	Hyp	Ref	Expression
1		ax-17 969	. . . 4 ⊢ (A ∈ D → ∀y A ∈ D)
2		ax-17 969	. . . . 5 ⊢ (z ∈ A → ∀y z ∈ A)
3	2	hbcsb1g 2020	. . . 4 ⊢ (A ∈ D → (z ∈ [A / y][y / x]B → ∀y z ∈ [A / y][y / x]B))
4	2	hbcsb1g 2020	. . . 4 ⊢ (A ∈ D → (z ∈ [A / y][y / x]R → ∀y z ∈ [A / y][y / x]R))
5	2	hbcsb1g 2020	. . . 4 ⊢ (A ∈ D → (z ∈ [A / y][y / x]C → ∀y z ∈ [A / y][y / x]C))
6	1, 3, 4, 5	hbbrd 2655	. . 3 ⊢ (A ∈ D → ([A / y][y / x]B[A / y][y / x]R[A / y][y / x]C → ∀y[A / y][y / x]B[A / y][y / x]R[A / y][y / x]C))
7		a9e 1123	. . . . . 6 ⊢ ∃x x = y
8		visset 1809	. . . . . . . . 9 ⊢ y ∈ V
9		ax-17 969	. . . . . . . . . 10 ⊢ (z ∈ y → ∀x z ∈ y)
10	9	hbsbc1g 1944	. . . . . . . . 9 ⊢ (y ∈ V → ([y / x]BRC → ∀x[y / x]BRC))
11	8, 10	ax-mp 7	. . . . . . . 8 ⊢ ([y / x]BRC → ∀x[y / x]BRC)
12	8, 9	hbcsb1 2021	. . . . . . . . 9 ⊢ (z ∈ [y / x]B → ∀x z ∈ [y / x]B)
13	8, 9	hbcsb1 2021	. . . . . . . . 9 ⊢ (z ∈ [y / x]R → ∀x z ∈ [y / x]R)
14	8, 9	hbcsb1 2021	. . . . . . . . 9 ⊢ (z ∈ [y / x]C → ∀x z ∈ [y / x]C)
15	12, 13, 14	hbbr 2654	. . . . . . . 8 ⊢ ([y / x]B[y / x]R[y / x]C → ∀x[y / x]B[y / x]R[y / x]C)
16	11, 15	hbbi 1008	. . . . . . 7 ⊢ (([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C) → ∀x([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C))
17		csbeq1a 2002	. . . . . . . . 9 ⊢ (x = y → B = [y / x]B)
18		csbeq1a 2002	. . . . . . . . 9 ⊢ (x = y → C = [y / x]C)
19	17, 18	breq12d 2627	. . . . . . . 8 ⊢ (x = y → (BRC ↔ [y / x]BR[y / x]C))
20		sbceq1a 1940	. . . . . . . 8 ⊢ (x = y → (BRC ↔ [y / x]BRC))
21		csbeq1a 2002	. . . . . . . . 9 ⊢ (x = y → R = [y / x]R)
22		breq 2617	. . . . . . . . 9 ⊢ (R = [y / x]R → ([y / x]BR[y / x]C ↔ [y / x]B[y / x]R[y / x]C))
23	21, 22	syl 10	. . . . . . . 8 ⊢ (x = y → ([y / x]BR[y / x]C ↔ [y / x]B[y / x]R[y / x]C))
24	19, 20, 23	3bitr3d 547	. . . . . . 7 ⊢ (x = y → ([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C))
25	16, 24	19.23ai 1062	. . . . . 6 ⊢ (∃x x = y → ([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C))
26	7, 25	ax-mp 7	. . . . 5 ⊢ ([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C)
27	26	a1i 8	. . . 4 ⊢ (y = A → ([y / x]BRC ↔ [y / x]B[y / x]R[y / x]C))
28		csbeq1a 2002	. . . . 5 ⊢ (y = A → [y / x]B = [A / y][y / x]B)
29		csbeq1a 2002	. . . . 5 ⊢ (y = A → [y / x]C = [A / y][y / x]C)
30	28, 29	breq12d 2627	. . . 4 ⊢ (y = A → ([y / x]B[y / x]R[y / x]C ↔ [A / y][y / x]B[y / x]R[A / y][y / x]C))
31		csbeq1a 2002	. . . . 5 ⊢ (y = A → [y / x]R = [A / y][y / x]R)
32		breq 2617	. . . . 5 ⊢ ([y / x]R = [A / y][y / x]R → ([A / y][y / x]B[y / x]R[A / y][y / x]C ↔ [A / y][y / x]B[A / y][y / x]R[A / y][y / x]C))
33	31, 32	syl 10	. . . 4 ⊢ (y = A → ([A / y][y / x]B[y / x]R[A / y][y / x]C ↔ [A / y][y / x]B[A / y][y / x]R[A / y][y / x]C))
34	27, 30, 33	3bitrd 543	. . 3 ⊢ (y = A → ([y / x]BRC ↔ [A / y][y / x]B[A / y][y / x]R[A / y][y / x]C))
35	6, 34	sbciegf 1956	. 2 ⊢ (A ∈ D → ([A / y][y / x]BRC ↔ [A / y][y / x]B[A / y][y / x]R[A / y][y / x]C))
36		sbccog 1948	. 2 ⊢ (A ∈ D → ([A / y][y / x]BRC ↔ [A / x]BRC))
37		csbcog 2003	. . . 4 ⊢ (A ∈ D → [A / y][y / x]B = [A / x]B)
38		csbcog 2003	. . . 4 ⊢ (A ∈ D → [A / y][y / x]C = [A / x]C)
39	37, 38	breq12d 2627	. . 3 ⊢ (A ∈ D → ([A / y][y / x]B[A / y][y / x]R[A / y][y / x]C ↔ [A / x]B[A / y][y / x]R[A / x]C))
40		csbcog 2003	. . . 4 ⊢ (A ∈ D → [A / y][y / x]R = [A / x]R)
41		breq 2617	. . . 4 ⊢ ([A / y][y / x]R = [A / x]R → ([A / x]B[A / y][y / x]R[A / x]C ↔ [A / x]B[A / x]R[A / x]C))
42	40, 41	syl 10	. . 3 ⊢ (A ∈ D → ([A / x]B[A / y][y / x]R[A / x]C ↔ [A / x]B[A / x]R[A / x]C))
43	39, 42	bitrd 527	. 2 ⊢ (A ∈ D → ([A / y][y / x]B[A / y][y / x]R[A / y][y / x]C ↔ [A / x]B[A / x]R[A / x]C))
44	35, 36, 43	3bitr3d 547	1 ⊢ (A ∈ D → ([A / x]BRC ↔ [A / x]B[A / x]R[A / x]C))

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  Vcvv 1807  [csb 1997   class class class wbr 2615

This theorem is referenced by:  sbcbr12g 2659

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  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2616

Copyright terms: Public domain