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

Theorem dfoprab2 6113
 Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
dfoprab2
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hints:   (,,)

Proof of Theorem dfoprab2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 excom 1756 . . . 4
2 exrot4 1760 . . . . 5
3 opeq1 3976 . . . . . . . . . . . 12
43eqeq2d 2446 . . . . . . . . . . 11
54pm5.32ri 620 . . . . . . . . . 10
65anbi1i 677 . . . . . . . . 9
7 anass 631 . . . . . . . . 9
8 an32 774 . . . . . . . . 9
96, 7, 83bitr3i 267 . . . . . . . 8
109exbii 1592 . . . . . . 7
11 opex 4419 . . . . . . . . 9
1211isseti 2954 . . . . . . . 8
13 19.42v 1928 . . . . . . . 8
1412, 13mpbiran2 886 . . . . . . 7
1510, 14bitri 241 . . . . . 6
16153exbii 1594 . . . . 5
172, 16bitri 241 . . . 4
18 19.42vv 1930 . . . . 5
19182exbii 1593 . . . 4
201, 17, 193bitr3i 267 . . 3
2120abbii 2547 . 2
22 df-oprab 6077 . 2
23 df-opab 4259 . 2
2421, 22, 233eqtr4i 2465 1
 Colors of variables: wff set class Syntax hints:   wa 359  wex 1550   wceq 1652  cab 2421  cop 3809  copab 4257  coprab 6074 This theorem is referenced by:  reloprab  6114  cbvoprab1  6136  cbvoprab12  6138  cbvoprab3  6140  dmoprab  6146  rnoprab  6148  ssoprab2i  6154  mpt2mptx  6156  resoprab  6158  funoprabg  6161  ov6g  6203  dfoprab3s  6394  xpcomco  7190  omxpenlem  7201  nvss  22064 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 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395 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-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-opab 4259  df-oprab 6077
 Copyright terms: Public domain W3C validator