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

Theorem abbii 2231
Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
abbii  |-  { x  |  ph }  =  {
x  |  ps }

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2229 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1411 1  |-  { x  |  ph }  =  {
x  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1314   {cab 2101
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108
This theorem is referenced by:  rabswap  2584  rabbiia  2643  rabab  2679  csb2  2975  cbvcsb  2977  csbid  2980  csbco  2982  cbvreucsf  3032  unrab  3315  inrab  3316  inrab2  3317  difrab  3318  rabun2  3323  dfnul3  3334  rab0  3359  tprot  3584  pw0  3635  dfuni2  3706  unipr  3718  dfint2  3741  int0  3753  dfiunv2  3817  cbviun  3818  cbviin  3819  iunrab  3828  iunid  3836  viin  3840  cbvopab  3967  cbvopab1  3969  cbvopab2  3970  cbvopab1s  3971  cbvopab2v  3973  unopab  3975  iunopab  4171  abnex  4336  uniuni  4340  ruv  4433  rabxp  4544  dfdm3  4694  dfrn2  4695  dfrn3  4696  dfdm4  4699  dfdmf  4700  dmun  4714  dmopab  4718  dmopabss  4719  dmopab3  4720  dfrnf  4748  rnopab  4754  rnmpt  4755  dfima2  4851  dfima3  4852  imadmrn  4859  imai  4863  args  4876  mptpreima  5000  dfiota2  5057  cbviota  5061  sb8iota  5063  dffv4g  5384  dfimafn2  5437  fnasrn  5564  fnasrng  5566  elabrex  5625  abrexco  5626  dfoprab2  5784  cbvoprab2  5810  dmoprab  5818  rnoprab  5820  rnoprab2  5821  fnrnov  5882  abrexex2g  5984  abrexex2  5988  abexssex  5989  abexex  5990  oprabrexex2  5994  dfopab2  6053  cnvoprab  6097  tfr1onlemaccex  6211  tfrcllemaccex  6224  tfrcldm  6226  frec0g  6260  frecsuc  6270  snec  6456  pmex  6513  dfixp  6560  cbvixp  6575  caucvgprprlemmu  7467  caucvgsr  7574  pitonnlem1  7617  mertenslem2  11245  toponsspwpwg  12084  tgval2  12115  bdcuni  12897  bj-dfom  12954
  Copyright terms: Public domain W3C validator