Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isrngo Unicode version

Theorem isrngo 21949
 Description: The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeffrey Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
isring.1
Assertion
Ref Expression
isrngo
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem isrngo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 4200 . . . 4
2 relrngo 21948 . . . . 5
32brrelexi 4904 . . . 4
41, 3sylbir 205 . . 3
54a1i 11 . 2
6 elex 2951 . . . 4
87a1i 11 . 2
9 df-rngo 21947 . . . . 5
109eleq2i 2494 . . . 4
11 simpl 444 . . . . . . . 8
1211eleq1d 2496 . . . . . . 7
13 simpr 448 . . . . . . . 8
1411rneqd 5083 . . . . . . . . . 10
15 isring.1 . . . . . . . . . 10
1614, 15syl6eqr 2480 . . . . . . . . 9
1716, 16xpeq12d 4889 . . . . . . . 8
1813, 17, 16feq123d 5569 . . . . . . 7
1912, 18anbi12d 692 . . . . . 6
2013oveqd 6084 . . . . . . . . . . . . 13
21 eqidd 2431 . . . . . . . . . . . . 13
2213, 20, 21oveq123d 6088 . . . . . . . . . . . 12
23 eqidd 2431 . . . . . . . . . . . . 13
2413oveqd 6084 . . . . . . . . . . . . 13
2513, 23, 24oveq123d 6088 . . . . . . . . . . . 12
2622, 25eqeq12d 2444 . . . . . . . . . . 11
2711oveqd 6084 . . . . . . . . . . . . 13
2813, 23, 27oveq123d 6088 . . . . . . . . . . . 12
2913oveqd 6084 . . . . . . . . . . . . 13
3011, 20, 29oveq123d 6088 . . . . . . . . . . . 12
3128, 30eqeq12d 2444 . . . . . . . . . . 11
3211oveqd 6084 . . . . . . . . . . . . 13
3313, 32, 21oveq123d 6088 . . . . . . . . . . . 12
3411, 29, 24oveq123d 6088 . . . . . . . . . . . 12
3533, 34eqeq12d 2444 . . . . . . . . . . 11
3626, 31, 353anbi123d 1254 . . . . . . . . . 10
3716, 36raleqbidv 2903 . . . . . . . . 9
3816, 37raleqbidv 2903 . . . . . . . 8
3916, 38raleqbidv 2903 . . . . . . 7
4020eqeq1d 2438 . . . . . . . . . 10
4113oveqd 6084 . . . . . . . . . . 11
4241eqeq1d 2438 . . . . . . . . . 10
4340, 42anbi12d 692 . . . . . . . . 9
4416, 43raleqbidv 2903 . . . . . . . 8
4516, 44rexeqbidv 2904 . . . . . . 7
4639, 45anbi12d 692 . . . . . 6
4719, 46anbi12d 692 . . . . 5
4847opelopabga 4455 . . . 4
4910, 48syl5bb 249 . . 3
5049expcom 425 . 2
515, 8, 50pm5.21ndd 344 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2692  wrex 2693  cvv 2943  cop 3804   class class class wbr 4199  copab 4252   cxp 4862   crn 4865  wf 5436  (class class class)co 6067  cablo 21852  crngo 21946 This theorem is referenced by:  isrngod  21950  rngoi  21951  cnrngo  21974 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-fv 5448  df-ov 6070  df-rngo 21947
 Copyright terms: Public domain W3C validator