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

Theorem abbii 2233
Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbii.1 (𝜑𝜓)
Assertion
Ref Expression
abbii {𝑥𝜑} = {𝑥𝜓}

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2231 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1413 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1316  {cab 2103
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
This theorem is referenced by:  rabswap  2586  rabbiia  2645  rabab  2681  csb2  2977  cbvcsb  2979  csbid  2982  csbco  2984  cbvreucsf  3034  unrab  3317  inrab  3318  inrab2  3319  difrab  3320  rabun2  3325  dfnul3  3336  rab0  3361  tprot  3586  pw0  3637  dfuni2  3708  unipr  3720  dfint2  3743  int0  3755  dfiunv2  3819  cbviun  3820  cbviin  3821  iunrab  3830  iunid  3838  viin  3842  cbvopab  3969  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab2v  3975  unopab  3977  iunopab  4173  abnex  4338  uniuni  4342  ruv  4435  rabxp  4546  dfdm3  4696  dfrn2  4697  dfrn3  4698  dfdm4  4701  dfdmf  4702  dmun  4716  dmopab  4720  dmopabss  4721  dmopab3  4722  dfrnf  4750  rnopab  4756  rnmpt  4757  dfima2  4853  dfima3  4854  imadmrn  4861  imai  4865  args  4878  mptpreima  5002  dfiota2  5059  cbviota  5063  sb8iota  5065  dffv4g  5386  dfimafn2  5439  fnasrn  5566  fnasrng  5568  elabrex  5627  abrexco  5628  dfoprab2  5786  cbvoprab2  5812  dmoprab  5820  rnoprab  5822  rnoprab2  5823  fnrnov  5884  abrexex2g  5986  abrexex2  5990  abexssex  5991  abexex  5992  oprabrexex2  5996  dfopab2  6055  cnvoprab  6099  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcldm  6228  frec0g  6262  frecsuc  6272  snec  6458  pmex  6515  dfixp  6562  cbvixp  6577  caucvgprprlemmu  7471  caucvgsr  7578  pitonnlem1  7621  mertenslem2  11260  toponsspwpwg  12100  tgval2  12131  bdcuni  12970  bj-dfom  13027
  Copyright terms: Public domain W3C validator