Theorem rabbii 3414

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3408

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 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rab 3409

This theorem is referenced by:  rabbieq  3417  dfdif3OLD  4084  elneldisj  4358  elnelun  4359  dfepfr  5625  epfrc  5626  fndmdifcom  7018  fniniseg2  7037  uniordint  7780  naddov3  8647  dfoi  9471  kmlem3  10113  alephsuc3  10540  hashbclem  14424  gcdcom  16490  gcdass  16524  lcmcom  16570  lcmass  16591  acsfn0  17628  dfinito2  17972  dftermo2  17973  dfrhm2  20390  lbsextg  21079  dmtopon  22817  fctop2  22899  ordtrest2  23098  qtopres  23592  tsmsfbas  24022  shftmbl  25446  ppiub  27122  rpvmasum  27444  noextendlt  27588  nosepne  27599  nosepdm  27603  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem4  27655  umgrislfupgrlem  29056  finsumvtxdg2ssteplem1  29480  clwwlknclwwlkdifnum  29916  clwwlknon2num  30041  dlwwlknondlwlknonf1o  30301  numclwlk1lem1  30305  3unrab  32439  aciunf1  32594  fpwrelmapffslem  32662  constrcbvlem  33752  ordtrest2NEW  33920  unelldsys  34155  rossros  34177  aean  34241  orvcval2  34457  subfacp1lem6  35179  satfv1  35357  itg2addnclem2  37673  scottexf  38169  scott0f  38170  refsymrels2  38563  dfeqvrels2  38586  refrelsredund3  38632  dffunsALTV5  38686  glbconxN  39379  primrootsunit1  42092  primrootsunit  42093  3anrabdioph  42777  3orrabdioph  42778  rexrabdioph  42789  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  elnn0rabdioph  42798  elnnrabdioph  42802  rabren3dioph  42810  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  onuniintrab  43222  relintab  43579  sqrtcvallem1  43627  uzmptshftfval  44342  binomcxplemdvsum  44351  binomcxp  44353  dvnprod  45954  ovnsubadd  46577  hoidmv1lelem3  46598  hoidmvlelem3  46602  ovolval3  46652  ovolval4lem2  46655  ovolval5lem3  46659  smflimlem4  46779