Theorem rabbii 3418

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

Syntax hints:   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is referenced by:  rabbieq  3421  dfdif3OLD  4070  dfepfr  5627  epfrc  5628  fndmdifcom  7019  fniniseg2  7038  uniordint  7779  naddov3  8645  dfoi  9453  kmlem3  10103  alephsuc3  10532  hashbclem  14459  gcdcom  16538  gcdass  16572  lcmcom  16618  lcmass  16639  acsfn0  17683  dfinito2  18027  dftermo2  18028  dfrhm2  20510  lbsextg  21220  dmtopon  22971  fctop2  23053  ordtrest2  23252  qtopres  23746  tsmsfbas  24176  shftmbl  25588  ppiub  27256  rpvmasum  27578  noextendlt  27721  nosepne  27732  nosepdm  27736  nosupbnd2lem1  27767  noinfbnd2lem1  27782  noetasuplem4  27788  umgrislfupgrlem  29280  finsumvtxdg2ssteplem1  29703  clwwlknclwwlkdifnum  30139  clwwlknon2num  30264  dlwwlknondlwlknonf1o  30524  numclwlk1lem1  30528  3unrab  32662  aciunf1  32826  fpwrelmapffslem  32895  constrcbvlem  34013  ordtrest2NEW  34181  unelldsys  34416  rossros  34438  aean  34502  orvcval2  34717  subfacp1lem6  35496  satfv1  35674  itg2addnclem2  38132  scottexf  38628  scott0f  38629  refsymrels2  39109  dfeqvrels2  39132  refrelsredund3  39178  dffunsALTV5  39232  glbconxN  39963  primrootsunit1  42675  primrootsunit  42676  3anrabdioph  43324  3orrabdioph  43325  rexrabdioph  43332  2rexfrabdioph  43334  3rexfrabdioph  43335  4rexfrabdioph  43336  6rexfrabdioph  43337  7rexfrabdioph  43338  elnn0rabdioph  43341  elnnrabdioph  43345  rabren3dioph  43353  rmydioph  43552  rmxdioph  43554  expdiophlem2  43560  onuniintrab  43764  relintab  44120  sqrtcvallem1  44168  uzmptshftfval  44883  binomcxplemdvsum  44892  binomcxp  44894  dvnprod  46484  fourierdlem113  46754  ovnsubadd  47107  hoidmv1lelem3  47128  hoidmvlelem3  47132  ovolval3  47182  ovolval4lem2  47185  ovolval5lem3  47189  smflimlem4  47309