ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abbii Unicode 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  |-  ( ph  <->  ps )
Assertion
Ref Expression
abbii  |-  { x  |  ph }  =  {
x  |  ps }

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2167 . 2  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
2 abbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpgbi 1357 1  |-  { x  |  ph }  =  {
x  |  ps }
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  2881  cbvcsb  2883  csbid  2886  csbco  2888  cbvreucsf  2937  unrab  3235  inrab  3236  inrab2  3237  difrab  3238  rabun2  3243  dfnul3  3254  rab0  3273  tprot  3490  pw0  3538  dfuni2  3609  unipr  3621  dfint2  3644  int0  3656  dfiunv2  3720  cbviun  3721  cbviin  3722  iunrab  3731  iunid  3739  viin  3743  cbvopab  3855  cbvopab1  3857  cbvopab2  3858  cbvopab1s  3859  cbvopab2v  3861  unopab  3863  iunopab  4045  uniuni  4210  ruv  4301  rabxp  4407  dfdm3  4549  dfrn2  4550  dfrn3  4551  dfdm4  4554  dfdmf  4555  dmun  4569  dmopab  4573  dmopabss  4574  dmopab3  4575  dfrnf  4602  rnopab  4608  rnmpt  4609  dfima2  4697  dfima3  4698  imadmrn  4705  imai  4708  args  4721  mptpreima  4841  dfiota2  4895  cbviota  4899  sb8iota  4901  dffv4g  5202  dfimafn2  5250  fnasrn  5368  fnasrng  5370  elabrex  5424  abrexco  5425  dfoprab2  5579  cbvoprab2  5604  dmoprab  5612  rnoprab  5614  rnoprab2  5615  fnrnov  5673  abrexex2g  5774  abrexex2  5778  abexssex  5779  abexex  5780  oprabrexex2  5784  dfopab2  5842  cnvoprab  5882  frec0g  6013  frecsuc  6021  snec  6197  caucvgprprlemmu  6850  caucvgsr  6943  pitonnlem1  6978  bdcuni  10362  bj-dfom  10423
  Copyright terms: Public domain W3C validator