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

Theorem opabbii 3897
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
opabbii  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }

Proof of Theorem opabbii
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 eqid 2088 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 9 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 3896 . 2  |-  ( z  =  z  ->  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps } )
51, 4ax-mp 7 1  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1289   {copab 3890
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-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-opab 3892
This theorem is referenced by:  mptv  3927  fconstmpt  4473  xpundi  4482  xpundir  4483  inxp  4558  cnvco  4609  resopab  4743  opabresid  4752  cnvi  4823  cnvun  4824  cnvin  4826  cnvxp  4837  cnvcnv3  4867  coundi  4919  coundir  4920  mptun  5130  fvopab6  5380  cbvoprab1  5702  cbvoprab12  5704  dmoprabss  5712  mpt2mptx  5721  resoprab  5723  ov6g  5764  dfoprab3s  5942  dfoprab3  5943  dfoprab4  5944  mapsncnv  6432  xpcomco  6522  dmaddpq  6917  dmmulpq  6918  recmulnqg  6929  enq0enq  6969  ltrelxr  7526  ltxr  9215  shftidt2  10231
  Copyright terms: Public domain W3C validator