Theorem rabbii 3421

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is used by:  rabbieq  3424  dfepfr  5642  epfrc  5643  fndmdifcom  7073  fniniseg2  7093  uniordint  7849  naddov3  8728  dfoi  9542  kmlem3  10270  alephsuc3  10704  hashbclem  14638  gcdcom  16729  gcdass  16764  lcmcom  16812  lcmass  16833  acsfn0  17884  dfinito2  18228  dftermo2  18229  dfrhm2  20755  lbsextg  21491  dmtopon  23296  fctop2  23378  ordtrest2  23577  qtopres  24072  tsmsfbas  24502  shftmbl  25914  ppiub  27588  rpvmasum  27910  noextendlt  28083  nosepne  28094  nosepdm  28098  nosupbnd2lem1  28129  noinfbnd2lem1  28144  noetasuplem4  28150  umgrislfupgrlem  29757  finsumvtxdg2ssteplem1  30183  clwwlknclwwlkdifnum  30628  clwwlknon2num  30753  dlwwlknondlwlknonf1o  31023  numclwlk1lem1  31027  3unrab  33198  aciunf1  33355  fpwrelmapffslem  33420  constrcbvlem  34498  ordtrest2NEW  34666  unelldsys  34902  rossros  34924  aean  34988  orvcval2  35202  subfacp1lem6  36158  satfv1  36336  itg2addnclem2  38858  scottexf  39366  scott0f  39367  refsymrels2  39847  dfeqvrels2  39870  refrelsredund3  39916  dffunsALTV5  39970  glbconxN  40701  primrootsunit1  43413  primrootsunit  43414  3anrabdioph  44059  3orrabdioph  44060  rexrabdioph  44067  2rexfrabdioph  44069  3rexfrabdioph  44070  4rexfrabdioph  44071  6rexfrabdioph  44072  7rexfrabdioph  44073  elnn0rabdioph  44076  elnnrabdioph  44080  rabren3dioph  44088  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  onuniintrab  44489  relintab  44845  sqrtcvallem1  44892  uzmptshftfval  45591  binomcxplemdvsum  45600  binomcxp  45602  dvnprod  47232  fourierdlem113  47502  ovnsubadd  47855  hoidmv1lelem3  47876  hoidmvlelem3  47880  ovolval3  47930  ovolval4lem2  47933  ovolval5lem3  47937  smflimlem4  48057