Theorem abbii 2255

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

Step	Hyp	Ref	Expression
1		abbi 2253	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpgbi 1428	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 104   = wceq 1331  {cab 2125

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132

This theorem is referenced by:  rabswap  2609  rabbiia  2671  rabab  2707  csb2  3005  cbvcsbw  3007  cbvcsb  3008  csbid  3011  csbco  3013  cbvreucsf  3064  unrab  3347  inrab  3348  inrab2  3349  difrab  3350  rabun2  3355  dfnul3  3366  rab0  3391  tprot  3616  pw0  3667  dfuni2  3738  unipr  3750  dfint2  3773  int0  3785  dfiunv2  3849  cbviun  3850  cbviin  3851  iunrab  3860  iunid  3868  viin  3872  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab2v  4005  unopab  4007  iunopab  4203  abnex  4368  uniuni  4372  ruv  4465  rabxp  4576  dfdm3  4726  dfrn2  4727  dfrn3  4728  dfdm4  4731  dfdmf  4732  dmun  4746  dmopab  4750  dmopabss  4751  dmopab3  4752  dfrnf  4780  rnopab  4786  rnmpt  4787  dfima2  4883  dfima3  4884  imadmrn  4891  imai  4895  args  4908  mptpreima  5032  dfiota2  5089  cbviota  5093  sb8iota  5095  dffv4g  5418  dfimafn2  5471  fnasrn  5598  fnasrng  5600  elabrex  5659  abrexco  5660  dfoprab2  5818  cbvoprab2  5844  dmoprab  5852  rnoprab  5854  rnoprab2  5855  fnrnov  5916  abrexex2g  6018  abrexex2  6022  abexssex  6023  abexex  6024  oprabrexex2  6028  dfopab2  6087  cnvoprab  6131  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcldm  6260  frec0g  6294  frecsuc  6304  snec  6490  pmex  6547  dfixp  6594  cbvixp  6609  caucvgprprlemmu  7503  caucvgsr  7610  pitonnlem1  7653  mertenslem2  11305  toponsspwpwg  12189  tgval2  12220  bdcuni  13074  bj-dfom  13131