Theorem rabbii 3397

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

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {crab 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-rab 3393

This theorem is referenced by:  rabbieq  3400  dfdif3OLD  4056  dfepfr  5609  epfrc  5610  fndmdifcom  6991  fniniseg2  7010  uniordint  7751  naddov3  8613  dfoi  9423  kmlem3  10073  alephsuc3  10501  hashbclem  14412  gcdcom  16480  gcdass  16514  lcmcom  16560  lcmass  16581  acsfn0  17624  dfinito2  17968  dftermo2  17969  dfrhm2  20452  lbsextg  21162  dmtopon  22913  fctop2  22995  ordtrest2  23194  qtopres  23688  tsmsfbas  24118  shftmbl  25530  ppiub  27192  rpvmasum  27514  noextendlt  27658  nosepne  27669  nosepdm  27673  nosupbnd2lem1  27704  noinfbnd2lem1  27719  noetasuplem4  27725  umgrislfupgrlem  29216  finsumvtxdg2ssteplem1  29639  clwwlknclwwlkdifnum  30075  clwwlknon2num  30200  dlwwlknondlwlknonf1o  30460  numclwlk1lem1  30464  3unrab  32598  aciunf1  32762  fpwrelmapffslem  32831  constrcbvlem  33946  ordtrest2NEW  34114  unelldsys  34349  rossros  34371  aean  34435  orvcval2  34650  subfacp1lem6  35420  satfv1  35598  itg2addnclem2  38046  scottexf  38542  scott0f  38543  refsymrels2  39023  dfeqvrels2  39046  refrelsredund3  39092  dffunsALTV5  39146  glbconxN  39877  primrootsunit1  42589  primrootsunit  42590  3anrabdioph  43238  3orrabdioph  43239  rexrabdioph  43246  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  elnn0rabdioph  43255  elnnrabdioph  43259  rabren3dioph  43267  rmydioph  43466  rmxdioph  43468  expdiophlem2  43474  onuniintrab  43678  relintab  44034  sqrtcvallem1  44082  uzmptshftfval  44797  binomcxplemdvsum  44806  binomcxp  44808  dvnprod  46399  ovnsubadd  47022  hoidmv1lelem3  47043  hoidmvlelem3  47047  ovolval3  47097  ovolval4lem2  47100  ovolval5lem3  47104  smflimlem4  47224