Theorem rabbii 3373

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

Syntax hints:   ↔ wb 209   = wceq 1543   ∈ wcel 2112  {crab 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-rab 3060

This theorem is referenced by:  dfdif3  4015  elneldisj  4289  elnelun  4290  dfepfr  5521  epfrc  5522  fndmdifcom  6841  fniniseg2  6860  uniordint  7563  dfoi  9105  kmlem3  9731  alephsuc3  10159  hashbclem  13981  gcdcom  16035  gcdass  16070  lcmcom  16113  lcmass  16134  acsfn0  17117  dfinito2  17463  dftermo2  17464  dfrhm2  19691  lbsextg  20153  dmtopon  21774  fctop2  21856  ordtrest2  22055  qtopres  22549  tsmsfbas  22979  shftmbl  24389  ppiub  26039  rpvmasum  26361  umgrislfupgrlem  27167  finsumvtxdg2ssteplem1  27587  clwwlknclwwlkdifnum  28017  clwwlknon2num  28142  dlwwlknondlwlknonf1o  28402  numclwlk1lem1  28406  aciunf1  30674  fpwrelmapffslem  30741  ordtrest2NEW  31541  unelldsys  31792  rossros  31814  aean  31878  orvcval2  32091  subfacp1lem6  32814  satfv1  32992  noextendlt  33558  nosepne  33569  nosepdm  33573  nosupbnd2lem1  33604  noinfbnd2lem1  33619  noetasuplem4  33625  itg2addnclem2  35515  scottexf  36012  scott0f  36013  rabbieq  36076  refsymrels2  36365  dfeqvrels2  36387  refrelsredund3  36433  dffunsALTV5  36484  glbconxN  37078  3anrabdioph  40248  3orrabdioph  40249  rexrabdioph  40260  2rexfrabdioph  40262  3rexfrabdioph  40263  4rexfrabdioph  40264  6rexfrabdioph  40265  7rexfrabdioph  40266  elnn0rabdioph  40269  elnnrabdioph  40273  rabren3dioph  40281  rmydioph  40480  rmxdioph  40482  expdiophlem2  40488  relintab  40808  sqrtcvallem1  40856  uzmptshftfval  41578  binomcxplemdvsum  41587  binomcxp  41589  dvnprod  43108  ovnsubadd  43728  hoidmv1lelem3  43749  hoidmvlelem3  43753  ovolval3  43803  ovolval4lem2  43806  ovolval5lem3  43810  smflimlem4  43924