Theorem rabbii 3417

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  rabbieq  3420  dfepfr  5639  epfrc  5640  fndmdifcom  7035  fniniseg2  7054  uniordint  7800  naddov3  8669  dfoi  9483  kmlem3  10155  alephsuc3  10589  hashbclem  14517  gcdcom  16603  gcdass  16637  lcmcom  16683  lcmass  16704  acsfn0  17748  dfinito2  18092  dftermo2  18093  dfrhm2  20615  lbsextg  21349  dmtopon  23148  fctop2  23230  ordtrest2  23429  qtopres  23924  tsmsfbas  24354  shftmbl  25766  ppiub  27440  rpvmasum  27762  noextendlt  27905  nosepne  27916  nosepdm  27920  nosupbnd2lem1  27951  noinfbnd2lem1  27966  noetasuplem4  27972  umgrislfupgrlem  29579  finsumvtxdg2ssteplem1  30005  clwwlknclwwlkdifnum  30450  clwwlknon2num  30575  dlwwlknondlwlknonf1o  30845  numclwlk1lem1  30849  3unrab  32978  aciunf1  33136  fpwrelmapffslem  33203  constrcbvlem  34265  ordtrest2NEW  34433  unelldsys  34669  rossros  34691  aean  34755  orvcval2  34970  subfacp1lem6  35764  satfv1  35942  itg2addnclem2  38421  scottexf  38916  scott0f  38917  refsymrels2  39397  dfeqvrels2  39420  refrelsredund3  39466  dffunsALTV5  39520  glbconxN  40251  primrootsunit1  42963  primrootsunit  42964  3anrabdioph  43627  3orrabdioph  43628  rexrabdioph  43635  2rexfrabdioph  43637  3rexfrabdioph  43638  4rexfrabdioph  43639  6rexfrabdioph  43640  7rexfrabdioph  43641  elnn0rabdioph  43644  elnnrabdioph  43648  rabren3dioph  43656  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  onuniintrab  44067  relintab  44423  sqrtcvallem1  44471  uzmptshftfval  45170  binomcxplemdvsum  45179  binomcxp  45181  dvnprod  46777  fourierdlem113  47047  ovnsubadd  47400  hoidmv1lelem3  47421  hoidmvlelem3  47425  ovolval3  47475  ovolval4lem2  47478  ovolval5lem3  47482  smflimlem4  47602