Theorem ecelqsi 6706

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		ecelqsg 6705	. 2 ⊢ ((𝑅 ∈ V ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
3	1, 2	mpan 424	1 ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))

Syntax hints:   → wi 4   ∈ wcel 2180  Vcvv 2779  [cec 6648   / cqs 6649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-xp 4702  df-cnv 4704  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-ec 6652  df-qs 6656

This theorem is referenced by:  ecopqsi  6707  th3q  6757  1nq  7521  addclnq  7530  mulclnq  7531  recexnq  7545  ltexnqq  7563  prarloclemarch  7573  prarloclemarch2  7574  nnnq  7577  nqnq0  7596  addnnnq0  7604  mulnnnq0  7605  addclnq0  7606  mulclnq0  7607  nqpnq0nq  7608  prarloclemlt  7648  prarloclemlo  7649  prarloclemcalc  7657  nqprm  7697  addsrpr  7900  mulsrpr  7901  0r  7905  1sr  7906  m1r  7907  addclsr  7908  mulclsr  7909  prsrcl  7939  mappsrprg  7959  suplocsrlemb  7961  pitonnlem2  8002  pitonn  8003  pitore  8005  recnnre  8006