Theorem rabbii 3395

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3390

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3391

This theorem is referenced by:  rabbieq  3398  dfdif3OLD  4059  dfepfr  5608  epfrc  5609  fndmdifcom  6989  fniniseg2  7008  uniordint  7748  naddov3  8609  dfoi  9419  kmlem3  10066  alephsuc3  10494  hashbclem  14405  gcdcom  16473  gcdass  16507  lcmcom  16553  lcmass  16574  acsfn0  17617  dfinito2  17961  dftermo2  17962  dfrhm2  20445  lbsextg  21152  dmtopon  22898  fctop2  22980  ordtrest2  23179  qtopres  23673  tsmsfbas  24103  shftmbl  25515  ppiub  27181  rpvmasum  27503  noextendlt  27647  nosepne  27658  nosepdm  27662  nosupbnd2lem1  27693  noinfbnd2lem1  27708  noetasuplem4  27714  umgrislfupgrlem  29205  finsumvtxdg2ssteplem1  29629  clwwlknclwwlkdifnum  30065  clwwlknon2num  30190  dlwwlknondlwlknonf1o  30450  numclwlk1lem1  30454  3unrab  32588  aciunf1  32751  fpwrelmapffslem  32820  constrcbvlem  33915  ordtrest2NEW  34083  unelldsys  34318  rossros  34340  aean  34404  orvcval2  34619  subfacp1lem6  35383  satfv1  35561  itg2addnclem2  38007  scottexf  38503  scott0f  38504  refsymrels2  38984  dfeqvrels2  39007  refrelsredund3  39053  dffunsALTV5  39107  glbconxN  39838  primrootsunit1  42550  primrootsunit  42551  3anrabdioph  43228  3orrabdioph  43229  rexrabdioph  43240  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  elnn0rabdioph  43249  elnnrabdioph  43253  rabren3dioph  43261  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  onuniintrab  43672  relintab  44028  sqrtcvallem1  44076  uzmptshftfval  44791  binomcxplemdvsum  44800  binomcxp  44802  dvnprod  46395  ovnsubadd  47018  hoidmv1lelem3  47039  hoidmvlelem3  47043  ovolval3  47093  ovolval4lem2  47096  ovolval5lem3  47100  smflimlem4  47220