ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ecelqsi GIF version

Theorem ecelqsi 6279
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
StepHypRef Expression
1 ecelqsi.1 . 2 𝑅 ∈ V
2 ecelqsg 6278 . 2 ((𝑅 ∈ V ∧ 𝐵𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
31, 2mpan 415 1 (𝐵𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  Vcvv 2614  [cec 6223   / cqs 6224
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-pow 3977  ax-pr 4003  ax-un 4227
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2616  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-br 3815  df-opab 3869  df-xp 4410  df-cnv 4412  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-ec 6227  df-qs 6231
This theorem is referenced by:  ecopqsi  6280  th3q  6330  1nq  6846  addclnq  6855  mulclnq  6856  recexnq  6870  ltexnqq  6888  prarloclemarch  6898  prarloclemarch2  6899  nnnq  6902  nqnq0  6921  addnnnq0  6929  mulnnnq0  6930  addclnq0  6931  mulclnq0  6932  nqpnq0nq  6933  prarloclemlt  6973  prarloclemlo  6974  prarloclemcalc  6982  nqprm  7022  addsrpr  7212  mulsrpr  7213  0r  7217  1sr  7218  m1r  7219  addclsr  7220  mulclsr  7221  prsrcl  7250  pitonnlem2  7305  pitonn  7306  pitore  7308  recnnre  7309
  Copyright terms: Public domain W3C validator