Theorem rabbii 3404

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3406. (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 3403	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  rabbieq  3407  dfdif3OLD  4070  elneldisj  4344  elnelun  4345  dfepfr  5608  epfrc  5609  fndmdifcom  6988  fniniseg2  7007  uniordint  7746  naddov3  8608  dfoi  9416  kmlem3  10063  alephsuc3  10491  hashbclem  14375  gcdcom  16440  gcdass  16474  lcmcom  16520  lcmass  16541  acsfn0  17583  dfinito2  17927  dftermo2  17928  dfrhm2  20410  lbsextg  21117  dmtopon  22867  fctop2  22949  ordtrest2  23148  qtopres  23642  tsmsfbas  24072  shftmbl  25495  ppiub  27171  rpvmasum  27493  noextendlt  27637  nosepne  27648  nosepdm  27652  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem4  27704  umgrislfupgrlem  29195  finsumvtxdg2ssteplem1  29619  clwwlknclwwlkdifnum  30055  clwwlknon2num  30180  dlwwlknondlwlknonf1o  30440  numclwlk1lem1  30444  3unrab  32578  aciunf1  32741  fpwrelmapffslem  32811  constrcbvlem  33912  ordtrest2NEW  34080  unelldsys  34315  rossros  34337  aean  34401  orvcval2  34616  subfacp1lem6  35379  satfv1  35557  itg2addnclem2  37873  scottexf  38369  scott0f  38370  refsymrels2  38822  dfeqvrels2  38845  refrelsredund3  38891  dffunsALTV5  38946  glbconxN  39638  primrootsunit1  42351  primrootsunit  42352  3anrabdioph  43024  3orrabdioph  43025  rexrabdioph  43036  2rexfrabdioph  43038  3rexfrabdioph  43039  4rexfrabdioph  43040  6rexfrabdioph  43041  7rexfrabdioph  43042  elnn0rabdioph  43045  elnnrabdioph  43049  rabren3dioph  43057  rmydioph  43256  rmxdioph  43258  expdiophlem2  43264  onuniintrab  43468  relintab  43824  sqrtcvallem1  43872  uzmptshftfval  44587  binomcxplemdvsum  44596  binomcxp  44598  dvnprod  46193  ovnsubadd  46816  hoidmv1lelem3  46837  hoidmvlelem3  46841  ovolval3  46891  ovolval4lem2  46894  ovolval5lem3  46898  smflimlem4  47018