Theorem rabbii 3439

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-rab 3434

This theorem is referenced by:  rabbieq  3442  dfdif3OLD  4128  elneldisj  4398  elnelun  4399  dfepfr  5673  epfrc  5674  fndmdifcom  7063  fniniseg2  7082  uniordint  7821  naddov3  8717  dfoi  9549  kmlem3  10191  alephsuc3  10618  hashbclem  14488  gcdcom  16547  gcdass  16581  lcmcom  16627  lcmass  16648  acsfn0  17705  dfinito2  18057  dftermo2  18058  dfrhm2  20491  lbsextg  21182  dmtopon  22945  fctop2  23028  ordtrest2  23228  qtopres  23722  tsmsfbas  24152  shftmbl  25587  ppiub  27263  rpvmasum  27585  noextendlt  27729  nosepne  27740  nosepdm  27744  nosupbnd2lem1  27775  noinfbnd2lem1  27790  noetasuplem4  27796  umgrislfupgrlem  29154  finsumvtxdg2ssteplem1  29578  clwwlknclwwlkdifnum  30009  clwwlknon2num  30134  dlwwlknondlwlknonf1o  30394  numclwlk1lem1  30398  3unrab  32531  aciunf1  32680  fpwrelmapffslem  32750  ordtrest2NEW  33884  unelldsys  34139  rossros  34161  aean  34225  orvcval2  34440  subfacp1lem6  35170  satfv1  35348  itg2addnclem2  37659  scottexf  38155  scott0f  38156  refsymrels2  38547  dfeqvrels2  38570  refrelsredund3  38616  dffunsALTV5  38669  glbconxN  39361  primrootsunit1  42079  primrootsunit  42080  3anrabdioph  42770  3orrabdioph  42771  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  elnn0rabdioph  42791  elnnrabdioph  42795  rabren3dioph  42803  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  onuniintrab  43215  relintab  43573  sqrtcvallem1  43621  uzmptshftfval  44342  binomcxplemdvsum  44351  binomcxp  44353  dvnprod  45905  ovnsubadd  46528  hoidmv1lelem3  46549  hoidmvlelem3  46553  ovolval3  46603  ovolval4lem2  46606  ovolval5lem3  46610  smflimlem4  46730