Theorem rabbii 3423

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {crab 3418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rab 3419

This theorem is used by:  rabbieq  3426  dfepfr  5647  epfrc  5648  fndmdifcom  7042  fniniseg2  7061  uniordint  7802  naddov3  8669  dfoi  9476  kmlem3  10148  alephsuc3  10576  hashbclem  14502  gcdcom  16588  gcdass  16622  lcmcom  16668  lcmass  16689  acsfn0  17733  dfinito2  18077  dftermo2  18078  dfrhm2  20581  lbsextg  21315  dmtopon  23109  fctop2  23191  ordtrest2  23390  qtopres  23884  tsmsfbas  24314  shftmbl  25726  ppiub  27397  rpvmasum  27719  noextendlt  27862  nosepne  27873  nosepdm  27877  nosupbnd2lem1  27908  noinfbnd2lem1  27923  noetasuplem4  27929  umgrislfupgrlem  29501  finsumvtxdg2ssteplem1  29924  clwwlknclwwlkdifnum  30360  clwwlknon2num  30485  dlwwlknondlwlknonf1o  30745  numclwlk1lem1  30749  3unrab  32878  aciunf1  33037  fpwrelmapffslem  33106  constrcbvlem  34168  ordtrest2NEW  34336  unelldsys  34572  rossros  34594  aean  34658  orvcval2  34873  subfacp1lem6  35690  satfv1  35868  itg2addnclem2  38356  scottexf  38850  scott0f  38851  refsymrels2  39331  dfeqvrels2  39354  refrelsredund3  39400  dffunsALTV5  39454  glbconxN  40185  primrootsunit1  42897  primrootsunit  42898  3anrabdioph  43546  3orrabdioph  43547  rexrabdioph  43554  2rexfrabdioph  43556  3rexfrabdioph  43557  4rexfrabdioph  43558  6rexfrabdioph  43559  7rexfrabdioph  43560  elnn0rabdioph  43563  elnnrabdioph  43567  rabren3dioph  43575  rmydioph  43774  rmxdioph  43776  expdiophlem2  43782  onuniintrab  43986  relintab  44342  sqrtcvallem1  44390  uzmptshftfval  45089  binomcxplemdvsum  45098  binomcxp  45100  dvnprod  46696  fourierdlem113  46966  ovnsubadd  47319  hoidmv1lelem3  47340  hoidmvlelem3  47344  ovolval3  47394  ovolval4lem2  47397  ovolval5lem3  47401  smflimlem4  47521