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

Theorem abbii 2150
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 {xφ} = {xψ}

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2148 . 2 (x(φψ) ↔ {xφ} = {xψ})
2 abbii.1 . 2 (φψ)
31, 2mpgbi 1338 1 {xφ} = {xψ}
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1242  {cab 2023
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030
This theorem is referenced by:  rabswap  2482  rabbiia  2541  rabab  2569  csb2  2848  cbvcsb  2850  csbid  2853  csbco  2855  cbvreucsf  2904  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  rabun2  3210  dfnul3  3221  rab0  3240  tprot  3454  pw0  3502  dfuni2  3573  unipr  3585  dfint2  3608  int0  3620  dfiunv2  3684  cbviun  3685  cbviin  3686  iunrab  3695  iunid  3703  viin  3707  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  unopab  3827  iunopab  4009  uniuni  4149  ruv  4228  rabxp  4323  dfdm3  4465  dfrn2  4466  dfrn3  4467  dfdm4  4470  dfdmf  4471  dmun  4485  dmopab  4489  dmopabss  4490  dmopab3  4491  dfrnf  4518  rnopab  4524  rnmpt  4525  dfima2  4613  dfima3  4614  imadmrn  4621  imai  4624  args  4637  mptpreima  4757  dfiota2  4811  cbviota  4815  sb8iota  4817  dffv4g  5118  dfimafn2  5166  fnasrn  5284  fnasrng  5286  elabrex  5340  abrexco  5341  dfoprab2  5494  cbvoprab2  5519  dmoprab  5527  rnoprab  5529  rnoprab2  5530  fnrnov  5588  abrexex2g  5689  abrexex2  5693  abexssex  5694  abexex  5695  oprabrexex2  5699  dfopab2  5757  frec0g  5922  frecsuc  5930  snec  6103  pitonnlem1  6721  bdcuni  9311  bj-dfom  9367
  Copyright terms: Public domain W3C validator