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

Theorem opabbii 4004
 Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbii.1
Assertion
Ref Expression
opabbii

Proof of Theorem opabbii
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2140 . 2
2 opabbii.1 . . . 4
32a1i 9 . . 3
43opabbidv 4003 . 2
51, 4ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wb 104   wceq 1332  copab 3997 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-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-opab 3999 This theorem is referenced by:  mptv  4034  fconstmpt  4596  xpundi  4605  xpundir  4606  inxp  4683  cnvco  4734  resopab  4873  opabresid  4882  cnvi  4953  cnvun  4954  cnvin  4956  cnvxp  4967  cnvcnv3  4998  coundi  5050  coundir  5051  mptun  5264  fvopab6  5527  cbvoprab1  5853  cbvoprab12  5855  dmoprabss  5863  mpomptx  5872  resoprab  5877  ov6g  5918  dfoprab3s  6098  dfoprab3  6099  dfoprab4  6100  mapsncnv  6599  xpcomco  6730  dmaddpq  7234  dmmulpq  7235  recmulnqg  7246  enq0enq  7286  ltrelxr  7872  ltxr  9615  shftidt2  10659  lmfval  12423  lmbr  12444  cnmptid  12512
 Copyright terms: Public domain W3C validator