Theorem rabbii 3470

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3477. (Contributed by Peter Mazsa, 1-Nov-2019.)

Hypothesis

Ref	Expression
rabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rabbii	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rabbiia 3469	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 208   = wceq 1536   ∈ wcel 2113  {crab 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2799  df-cleq 2813  df-rab 3146

This theorem is referenced by:  dfdif3  4084  elneldisj  4335  elnelun  4336  dfepfr  5533  epfrc  5534  fndmdifcom  6806  fniniseg2  6825  uniordint  7514  dfoi  8968  kmlem3  9571  alephsuc3  9995  hashbclem  13807  gcdcom  15857  gcdass  15890  lcmcom  15932  lcmass  15953  acsfn0  16926  dfrhm2  19464  lbsextg  19929  dmtopon  21526  fctop2  21608  ordtrest2  21807  qtopres  22301  tsmsfbas  22731  shftmbl  24134  ppiub  25778  rpvmasum  26100  umgrislfupgrlem  26905  finsumvtxdg2ssteplem1  27325  clwwlknclwwlkdifnum  27756  clwwlknon2num  27882  dlwwlknondlwlknonf1o  28142  numclwlk1lem1  28146  aciunf1  30408  fpwrelmapffslem  30468  ordtrest2NEW  31187  unelldsys  31438  rossros  31460  aean  31524  orvcval2  31737  subfacp1lem6  32453  satfv1  32631  noextendlt  33197  nosepne  33206  nosepdm  33209  nosupbnd2lem1  33236  noetalem3  33240  itg2addnclem2  34979  scottexf  35479  scott0f  35480  rabbieq  35545  refsymrels2  35834  dfeqvrels2  35856  refrelsredund3  35902  dffunsALTV5  35953  glbconxN  36547  3anrabdioph  39455  3orrabdioph  39456  rexrabdioph  39467  2rexfrabdioph  39469  3rexfrabdioph  39470  4rexfrabdioph  39471  6rexfrabdioph  39472  7rexfrabdioph  39473  elnn0rabdioph  39476  elnnrabdioph  39480  rabren3dioph  39488  rmydioph  39687  rmxdioph  39689  expdiophlem2  39695  relintab  40017  uzmptshftfval  40752  binomcxplemdvsum  40761  binomcxp  40763  dvnprod  42308  ovnsubadd  42928  hoidmv1lelem3  42949  hoidmvlelem3  42953  ovolval3  43003  ovolval4lem2  43006  ovolval5lem3  43010  smflimlem4  43124