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 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

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

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is used by:  rabbieq  3421  dfepfr  5635  epfrc  5636  fndmdifcom  7040  fniniseg2  7059  uniordint  7813  naddov3  8683  dfoi  9498  kmlem3  10224  alephsuc3  10658  hashbclem  14590  gcdcom  16678  gcdass  16713  lcmcom  16761  lcmass  16782  acsfn0  17827  dfinito2  18171  dftermo2  18172  dfrhm2  20697  lbsextg  21433  dmtopon  23234  fctop2  23316  ordtrest2  23515  qtopres  24010  tsmsfbas  24440  shftmbl  25852  ppiub  27524  rpvmasum  27846  noextendlt  28019  nosepne  28030  nosepdm  28034  nosupbnd2lem1  28065  noinfbnd2lem1  28080  noetasuplem4  28086  umgrislfupgrlem  29693  finsumvtxdg2ssteplem1  30119  clwwlknclwwlkdifnum  30564  clwwlknon2num  30689  dlwwlknondlwlknonf1o  30959  numclwlk1lem1  30963  3unrab  33092  aciunf1  33250  fpwrelmapffslem  33317  constrcbvlem  34380  ordtrest2NEW  34548  unelldsys  34784  rossros  34806  aean  34870  orvcval2  35084  subfacp1lem6  35929  satfv1  36107  itg2addnclem2  38570  scottexf  39080  scott0f  39081  refsymrels2  39561  dfeqvrels2  39584  refrelsredund3  39630  dffunsALTV5  39684  glbconxN  40415  primrootsunit1  43127  primrootsunit  43128  3anrabdioph  43772  3orrabdioph  43773  rexrabdioph  43780  2rexfrabdioph  43782  3rexfrabdioph  43783  4rexfrabdioph  43784  6rexfrabdioph  43785  7rexfrabdioph  43786  elnn0rabdioph  43789  elnnrabdioph  43793  rabren3dioph  43801  rmydioph  44000  rmxdioph  44002  expdiophlem2  44008  onuniintrab  44212  relintab  44568  sqrtcvallem1  44616  uzmptshftfval  45315  binomcxplemdvsum  45324  binomcxp  45326  dvnprod  46928  fourierdlem113  47198  ovnsubadd  47551  hoidmv1lelem3  47572  hoidmvlelem3  47576  ovolval3  47626  ovolval4lem2  47629  ovolval5lem3  47633  smflimlem4  47753