Theorem rabbii 3406

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

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

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 3402

This theorem is referenced by:  rabbieq  3409  dfdif3OLD  4072  elneldisj  4346  elnelun  4347  dfepfr  5616  epfrc  5617  fndmdifcom  6997  fniniseg2  7016  uniordint  7756  naddov3  8618  dfoi  9428  kmlem3  10075  alephsuc3  10503  hashbclem  14387  gcdcom  16452  gcdass  16486  lcmcom  16532  lcmass  16553  acsfn0  17595  dfinito2  17939  dftermo2  17940  dfrhm2  20422  lbsextg  21129  dmtopon  22879  fctop2  22961  ordtrest2  23160  qtopres  23654  tsmsfbas  24084  shftmbl  25507  ppiub  27183  rpvmasum  27505  noextendlt  27649  nosepne  27660  nosepdm  27664  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetasuplem4  27716  umgrislfupgrlem  29207  finsumvtxdg2ssteplem1  29631  clwwlknclwwlkdifnum  30067  clwwlknon2num  30192  dlwwlknondlwlknonf1o  30452  numclwlk1lem1  30456  3unrab  32589  aciunf1  32752  fpwrelmapffslem  32821  constrcbvlem  33932  ordtrest2NEW  34100  unelldsys  34335  rossros  34357  aean  34421  orvcval2  34636  subfacp1lem6  35398  satfv1  35576  itg2addnclem2  37920  scottexf  38416  scott0f  38417  refsymrels2  38897  dfeqvrels2  38920  refrelsredund3  38966  dffunsALTV5  39020  glbconxN  39751  primrootsunit1  42464  primrootsunit  42465  3anrabdioph  43136  3orrabdioph  43137  rexrabdioph  43148  2rexfrabdioph  43150  3rexfrabdioph  43151  4rexfrabdioph  43152  6rexfrabdioph  43153  7rexfrabdioph  43154  elnn0rabdioph  43157  elnnrabdioph  43161  rabren3dioph  43169  rmydioph  43368  rmxdioph  43370  expdiophlem2  43376  onuniintrab  43580  relintab  43936  sqrtcvallem1  43984  uzmptshftfval  44699  binomcxplemdvsum  44708  binomcxp  44710  dvnprod  46304  ovnsubadd  46927  hoidmv1lelem3  46948  hoidmvlelem3  46952  ovolval3  47002  ovolval4lem2  47005  ovolval5lem3  47009  smflimlem4  47129