Theorem rabbii 3424

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {crab 3418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-rab 3419

This theorem is referenced by:  rabbieq  3427  dfdif3  4110  elneldisj  4390  elnelun  4391  dfepfr  5663  epfrc  5664  fndmdifcom  7051  fniniseg2  7070  uniordint  7805  naddov3  8701  dfoi  9541  kmlem3  10182  alephsuc3  10610  hashbclem  14452  gcdcom  16496  gcdass  16531  lcmcom  16572  lcmass  16593  acsfn0  17648  dfinito2  18000  dftermo2  18001  dfrhm2  20430  lbsextg  21067  dmtopon  22874  fctop2  22957  ordtrest2  23157  qtopres  23651  tsmsfbas  24081  shftmbl  25516  ppiub  27187  rpvmasum  27509  noextendlt  27653  nosepne  27664  nosepdm  27668  nosupbnd2lem1  27699  noinfbnd2lem1  27714  noetasuplem4  27720  umgrislfupgrlem  29012  finsumvtxdg2ssteplem1  29436  clwwlknclwwlkdifnum  29867  clwwlknon2num  29992  dlwwlknondlwlknonf1o  30252  numclwlk1lem1  30256  aciunf1  32535  fpwrelmapffslem  32601  ordtrest2NEW  33657  unelldsys  33910  rossros  33932  aean  33996  orvcval2  34211  subfacp1lem6  34928  satfv1  35106  itg2addnclem2  37278  scottexf  37774  scott0f  37775  refsymrels2  38169  dfeqvrels2  38192  refrelsredund3  38238  dffunsALTV5  38291  glbconxN  38983  primrootsunit1  41701  primrootsunit  41702  3anrabdioph  42346  3orrabdioph  42347  rexrabdioph  42358  2rexfrabdioph  42360  3rexfrabdioph  42361  4rexfrabdioph  42362  6rexfrabdioph  42363  7rexfrabdioph  42364  elnn0rabdioph  42367  elnnrabdioph  42371  rabren3dioph  42379  rmydioph  42579  rmxdioph  42581  expdiophlem2  42587  onuniintrab  42798  relintab  43157  sqrtcvallem1  43205  uzmptshftfval  43927  binomcxplemdvsum  43936  binomcxp  43938  dvnprod  45477  ovnsubadd  46100  hoidmv1lelem3  46121  hoidmvlelem3  46125  ovolval3  46175  ovolval4lem2  46178  ovolval5lem3  46182  smflimlem4  46302