Theorem ecelqsi 6523

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	|- R e. _V

Assertion

Ref	Expression
ecelqsi	|- ( B e. A -> [ B ] R e. ( A /. R ) )

Proof of Theorem ecelqsi

Step	Hyp	Ref	Expression
1		ecelqsi.1	. 2 |- R e. _V
2		ecelqsg 6522	. 2 |- ( ( R e. _V /\ B e. A ) -> [ B ] R e. ( A /. R ) )
3	1, 2	mpan 421	1 |- ( B e. A -> [ B ] R e. ( A /. R ) )

Syntax hints:   -> wi 4   e. wcel 2125   _Vcvv 2709   [cec 6467   /.cqs 6468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pow 4130  ax-pr 4164  ax-un 4388

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-rex 2438  df-v 2711  df-un 3102  df-in 3104  df-ss 3111  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-opab 4022  df-xp 4585  df-cnv 4587  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-ec 6471  df-qs 6475

This theorem is referenced by:  ecopqsi  6524  th3q  6574  1nq  7265  addclnq  7274  mulclnq  7275  recexnq  7289  ltexnqq  7307  prarloclemarch  7317  prarloclemarch2  7318  nnnq  7321  nqnq0  7340  addnnnq0  7348  mulnnnq0  7349  addclnq0  7350  mulclnq0  7351  nqpnq0nq  7352  prarloclemlt  7392  prarloclemlo  7393  prarloclemcalc  7401  nqprm  7441  addsrpr  7644  mulsrpr  7645  0r  7649  1sr  7650  m1r  7651  addclsr  7652  mulclsr  7653  prsrcl  7683  mappsrprg  7703  suplocsrlemb  7705  pitonnlem2  7746  pitonn  7747  pitore  7749  recnnre  7750