Theorem rabbii 3401

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-rab 3397

This theorem is referenced by:  rabbieq  3404  dfdif3OLD  4067  elneldisj  4341  elnelun  4342  dfepfr  5605  epfrc  5606  fndmdifcom  6985  fniniseg2  7004  uniordint  7743  naddov3  8604  dfoi  9408  kmlem3  10055  alephsuc3  10482  hashbclem  14366  gcdcom  16431  gcdass  16465  lcmcom  16511  lcmass  16532  acsfn0  17574  dfinito2  17918  dftermo2  17919  dfrhm2  20401  lbsextg  21108  dmtopon  22858  fctop2  22940  ordtrest2  23139  qtopres  23633  tsmsfbas  24063  shftmbl  25486  ppiub  27162  rpvmasum  27484  noextendlt  27628  nosepne  27639  nosepdm  27643  nosupbnd2lem1  27674  noinfbnd2lem1  27689  noetasuplem4  27695  umgrislfupgrlem  29121  finsumvtxdg2ssteplem1  29545  clwwlknclwwlkdifnum  29981  clwwlknon2num  30106  dlwwlknondlwlknonf1o  30366  numclwlk1lem1  30370  3unrab  32504  aciunf1  32667  fpwrelmapffslem  32739  constrcbvlem  33840  ordtrest2NEW  34008  unelldsys  34243  rossros  34265  aean  34329  orvcval2  34544  subfacp1lem6  35301  satfv1  35479  itg2addnclem2  37785  scottexf  38281  scott0f  38282  refsymrels2  38734  dfeqvrels2  38757  refrelsredund3  38803  dffunsALTV5  38858  glbconxN  39550  primrootsunit1  42263  primrootsunit  42264  3anrabdioph  42939  3orrabdioph  42940  rexrabdioph  42951  2rexfrabdioph  42953  3rexfrabdioph  42954  4rexfrabdioph  42955  6rexfrabdioph  42956  7rexfrabdioph  42957  elnn0rabdioph  42960  elnnrabdioph  42964  rabren3dioph  42972  rmydioph  43171  rmxdioph  43173  expdiophlem2  43179  onuniintrab  43383  relintab  43740  sqrtcvallem1  43788  uzmptshftfval  44503  binomcxplemdvsum  44512  binomcxp  44514  dvnprod  46109  ovnsubadd  46732  hoidmv1lelem3  46753  hoidmvlelem3  46757  ovolval3  46807  ovolval4lem2  46810  ovolval5lem3  46814  smflimlem4  46934