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

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

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2167 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1357 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff set class
Syntax hints:  wb 102   = wceq 1259  {cab 2042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049
This theorem is referenced by:  rabswap  2505  rabbiia  2564  rabab  2592  csb2  2882  cbvcsb  2884  csbid  2887  csbco  2889  cbvreucsf  2938  unrab  3236  inrab  3237  inrab2  3238  difrab  3239  rabun2  3244  dfnul3  3255  rab0  3274  tprot  3491  pw0  3539  dfuni2  3610  unipr  3622  dfint2  3645  int0  3657  dfiunv2  3721  cbviun  3722  cbviin  3723  iunrab  3732  iunid  3740  viin  3744  cbvopab  3856  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  cbvopab2v  3862  unopab  3864  iunopab  4046  uniuni  4211  ruv  4302  rabxp  4408  dfdm3  4550  dfrn2  4551  dfrn3  4552  dfdm4  4555  dfdmf  4556  dmun  4570  dmopab  4574  dmopabss  4575  dmopab3  4576  dfrnf  4603  rnopab  4609  rnmpt  4610  dfima2  4698  dfima3  4699  imadmrn  4706  imai  4709  args  4722  mptpreima  4842  dfiota2  4896  cbviota  4900  sb8iota  4902  dffv4g  5203  dfimafn2  5251  fnasrn  5369  fnasrng  5371  elabrex  5425  abrexco  5426  dfoprab2  5580  cbvoprab2  5605  dmoprab  5613  rnoprab  5615  rnoprab2  5616  fnrnov  5674  abrexex2g  5775  abrexex2  5779  abexssex  5780  abexex  5781  oprabrexex2  5785  dfopab2  5843  cnvoprab  5883  frec0g  6014  frecsuc  6022  snec  6198  caucvgprprlemmu  6851  caucvgsr  6944  pitonnlem1  6979  bdcuni  10383  bj-dfom  10444
  Copyright terms: Public domain W3C validator