Theorem rabbii 3411

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-rab 3406

This theorem is referenced by:  dfdif3  4079  elneldisj  4353  elnelun  4354  dfepfr  5623  epfrc  5624  fndmdifcom  6998  fniniseg2  7017  uniordint  7741  naddov3  8631  dfoi  9456  kmlem3  10097  alephsuc3  10525  hashbclem  14361  gcdcom  16404  gcdass  16439  lcmcom  16480  lcmass  16501  acsfn0  17554  dfinito2  17903  dftermo2  17904  dfrhm2  20164  lbsextg  20682  dmtopon  22309  fctop2  22392  ordtrest2  22592  qtopres  23086  tsmsfbas  23516  shftmbl  24939  ppiub  26589  rpvmasum  26911  noextendlt  27054  nosepne  27065  nosepdm  27069  nosupbnd2lem1  27100  noinfbnd2lem1  27115  noetasuplem4  27121  umgrislfupgrlem  28136  finsumvtxdg2ssteplem1  28556  clwwlknclwwlkdifnum  28987  clwwlknon2num  29112  dlwwlknondlwlknonf1o  29372  numclwlk1lem1  29376  aciunf1  31646  fpwrelmapffslem  31717  ordtrest2NEW  32593  unelldsys  32846  rossros  32868  aean  32932  orvcval2  33147  subfacp1lem6  33866  satfv1  34044  itg2addnclem2  36203  scottexf  36700  scott0f  36701  rabbieq  36783  refsymrels2  37100  dfeqvrels2  37123  refrelsredund3  37169  dffunsALTV5  37222  glbconxN  37914  3anrabdioph  41163  3orrabdioph  41164  rexrabdioph  41175  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  elnn0rabdioph  41184  elnnrabdioph  41188  rabren3dioph  41196  rmydioph  41396  rmxdioph  41398  expdiophlem2  41404  onuniintrab  41618  relintab  41977  sqrtcvallem1  42025  uzmptshftfval  42748  binomcxplemdvsum  42757  binomcxp  42759  dvnprod  44310  ovnsubadd  44933  hoidmv1lelem3  44954  hoidmvlelem3  44958  ovolval3  45008  ovolval4lem2  45011  ovolval5lem3  45015  smflimlem4  45135