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

Theorem opabbii 3965
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 2117 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 9 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 3964 . 2  |-  ( z  =  z  ->  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps } )
51, 4ax-mp 5 1  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1316   {copab 3958
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-opab 3960
This theorem is referenced by:  mptv  3995  fconstmpt  4556  xpundi  4565  xpundir  4566  inxp  4643  cnvco  4694  resopab  4833  opabresid  4842  cnvi  4913  cnvun  4914  cnvin  4916  cnvxp  4927  cnvcnv3  4958  coundi  5010  coundir  5011  mptun  5224  fvopab6  5485  cbvoprab1  5811  cbvoprab12  5813  dmoprabss  5821  mpomptx  5830  resoprab  5835  ov6g  5876  dfoprab3s  6056  dfoprab3  6057  dfoprab4  6058  mapsncnv  6557  xpcomco  6688  dmaddpq  7155  dmmulpq  7156  recmulnqg  7167  enq0enq  7207  ltrelxr  7793  ltxr  9517  shftidt2  10559  lmfval  12272  lmbr  12293  cnmptid  12361
  Copyright terms: Public domain W3C validator