Theorem ecelqsi 4282

Description: Membership of an equivalence class in a quotient set.

Hypothesis

Ref	Expression
ecelqsi.1	⊢ R ∈ V

Assertion

Ref	Expression
ecelqsi	⊢ (B ∈ A → [B]R ∈ (A / R))

Proof of Theorem ecelqsi

Step	Hyp	Ref	Expression
1		eceq2 4268	. . 3 ⊢ (y = B → [y]R = [B]R)
2	1	eleq1d 1537	. 2 ⊢ (y = B → ([y]R ∈ (A / R) ↔ [B]R ∈ (A / R)))
3		a9e 1123	. . . 4 ⊢ ∃x x = y
4		eqid 1473	. . . . . 6 ⊢ [y]R = [y]R
5		eleq1 1531	. . . . . . . 8 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
6		eceq2 4268	. . . . . . . . 9 ⊢ (x = y → [x]R = [y]R)
7	6	eqeq2d 1483	. . . . . . . 8 ⊢ (x = y → ([y]R = [x]R ↔ [y]R = [y]R))
8	5, 7	anbi12d 627	. . . . . . 7 ⊢ (x = y → ((x ∈ A ⋀ [y]R = [x]R) ↔ (y ∈ A ⋀ [y]R = [y]R)))
9	8	biimprcd 156	. . . . . 6 ⊢ ((y ∈ A ⋀ [y]R = [y]R) → (x = y → (x ∈ A ⋀ [y]R = [x]R)))
10	4, 9	mpan2 695	. . . . 5 ⊢ (y ∈ A → (x = y → (x ∈ A ⋀ [y]R = [x]R)))
11	10	19.22dv 1288	. . . 4 ⊢ (y ∈ A → (∃x x = y → ∃x(x ∈ A ⋀ [y]R = [x]R)))
12	3, 11	mpi 44	. . 3 ⊢ (y ∈ A → ∃x(x ∈ A ⋀ [y]R = [x]R))
13		ecelqsi.1	. . . . 5 ⊢ R ∈ V
14		ecexg 4255	. . . . 5 ⊢ (R ∈ V → [y]R ∈ V)
15	13, 14	ax-mp 7	. . . 4 ⊢ [y]R ∈ V
16	15	elqs 4280	. . 3 ⊢ ([y]R ∈ (A / R) ↔ ∃x(x ∈ A ⋀ [y]R = [x]R))
17	12, 16	sylibr 200	. 2 ⊢ (y ∈ A → [y]R ∈ (A / R))
18	2, 17	vtoclga 1848	1 ⊢ (B ∈ A → [B]R ∈ (A / R))

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 954   ∈ wcel 956  ∃wex 978  Vcvv 1807  [cec 4249   / cqs 4250

This theorem is referenced by:  ecopqsi 4283  th3q 4307  1q 5037  addclpq 5038  mulclpq 5040  0r 5169  1r 5170  m1r 5171  addclsr 5172  mulclsr 5173

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-13 967  ax-14 968  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  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-ec 4253  df-qs 4256

Copyright terms: Public domain