Theorem ecelqsi 8746

Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
ecelqsi.1	⊢ 𝑅 ∈ V

Assertion

Ref	Expression
ecelqsi	⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))

Proof of Theorem ecelqsi

Step	Hyp	Ref	Expression
1		ecelqsi.1	. 2 ⊢ 𝑅 ∈ V
2		ecelqsw 8745	. 2 ⊢ ((𝑅 ∈ V ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
3	1, 2	mpan 690	1 ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  [cec 8672   / cqs 8673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ec 8676  df-qs 8680

This theorem is referenced by:  ecopqsi  8747  addsrpr  11035  mulsrpr  11036  0r  11040  1sr  11041  m1r  11042  addclsr  11043  mulclsr  11044  quseccl0  19124  ghmqusnsglem1  19219  ghmquskerlem1  19222  ghmquskerco  19223  ghmqusker  19226  orbsta  19252  frgpeccl  19698  rngqiprngimf  21214  qustgphaus  24017  vitalilem2  25517  vitalilem3  25518  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  fracfld  33265  nsgqusf1olem1  33391  qsidomlem1  33430  qsdrngilem  33472  qsdrngi  33473  qsdrnglem2  33474  zringfrac  33532  pstmfval  33893