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

Theorem opabbii 4516
 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 2457 . 2
2 opabbii.1 . . . 4
32a1i 11 . . 3
43opabbidv 4515 . 2
51, 4ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  {copab 4509 This theorem is referenced by:  mptv  4544  fconstmpt  5048  xpundi  5057  xpundir  5058  inxp  5140  csbcnv  5191  cnvco  5193  resopab  5325  opabresid  5332  cnvi  5415  cnvun  5416  cnvxp  5429  cnvcnv3  5461  coundi  5513  coundir  5514  mptun  5717  fvopab6  5980  fmptsng  6092  fmptsnd  6093  cbvoprab1  6369  cbvoprab12  6371  dmoprabss  6384  mpt2mptx  6393  resoprab  6398  elrnmpt2res  6416  ov6g  6440  1st2val  6826  2nd2val  6827  dfoprab3s  6855  dfoprab3  6856  dfoprab4  6857  fsplit  6905  mapsncnv  7485  xpcomco  7627  marypha2lem2  7916  oemapso  8122  leweon  8410  r0weon  8411  compsscnv  8772  fpwwe  9045  ltrelxr  9669  ltxrlt  9676  ltxr  11353  shftidt2  12914  prdsle  14859  prdsless  14860  prdsleval  14874  joindm  15633  meetdm  15647  gaorb  16345  efgcpbllema  16772  frgpuplem  16790  ltbval  18136  ltbwe  18137  opsrle  18140  opsrtoslem1  18148  opsrtoslem2  18149  dvdsrzring  18507  dvdsrz  18508  pjfval2  18740  lmfval  19733  lmbr  19759  cnmptid  20162  lgsquadlem3  23631  perpln1  24087  axcontlem2  24268  wlks  24519  trls  24538  dfconngra1  24671  dfadj2  26804  dmadjss  26806  cnvadj  26811  mpt2mptxf  27518  dfid4  29103  fneer  30171  opropabco  30214  fgraphopab  31170  fgraphxp  31171  xpsnopab  32453  dfiso2  32568  mpt2mptx2  32924  cmtfvalN  34935  cmtvalN  34936  cvrfval  34993  cvrval  34994  dicval2  36906 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511
 Copyright terms: Public domain W3C validator