Theorem rabbii 3428

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424

This theorem is referenced by:  rabbieq  3431  dfdif3OLD  4081  dfepfr  5643  epfrc  5644  fndmdifcom  7036  fniniseg2  7055  uniordint  7796  naddov3  8663  dfoi  9469  kmlem3  10132  alephsuc3  10561  hashbclem  14485  gcdcom  16567  gcdass  16601  lcmcom  16647  lcmass  16668  acsfn0  17712  dfinito2  18056  dftermo2  18057  dfrhm2  20552  lbsextg  21260  dmtopon  23045  fctop2  23127  ordtrest2  23326  qtopres  23820  tsmsfbas  24250  shftmbl  25662  ppiub  27330  rpvmasum  27652  noextendlt  27795  nosepne  27806  nosepdm  27810  nosupbnd2lem1  27841  noinfbnd2lem1  27856  noetasuplem4  27862  umgrislfupgrlem  29409  finsumvtxdg2ssteplem1  29832  clwwlknclwwlkdifnum  30268  clwwlknon2num  30393  dlwwlknondlwlknonf1o  30653  numclwlk1lem1  30657  3unrab  32786  aciunf1  32945  fpwrelmapffslem  33014  constrcbvlem  34086  ordtrest2NEW  34254  unelldsys  34489  rossros  34511  aean  34575  orvcval2  34790  subfacp1lem6  35572  satfv1  35750  itg2addnclem2  38206  scottexf  38702  scott0f  38703  refsymrels2  39183  dfeqvrels2  39206  refrelsredund3  39252  dffunsALTV5  39306  glbconxN  40037  primrootsunit1  42749  primrootsunit  42750  3anrabdioph  43398  3orrabdioph  43399  rexrabdioph  43406  2rexfrabdioph  43408  3rexfrabdioph  43409  4rexfrabdioph  43410  6rexfrabdioph  43411  7rexfrabdioph  43412  elnn0rabdioph  43415  elnnrabdioph  43419  rabren3dioph  43427  rmydioph  43626  rmxdioph  43628  expdiophlem2  43634  onuniintrab  43838  relintab  44194  sqrtcvallem1  44242  uzmptshftfval  44941  binomcxplemdvsum  44950  binomcxp  44952  dvnprod  46548  fourierdlem113  46818  ovnsubadd  47171  hoidmv1lelem3  47192  hoidmvlelem3  47196  ovolval3  47246  ovolval4lem2  47249  ovolval5lem3  47253  smflimlem4  47373