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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is referenced by:  rabbieq  3424  dfdif3OLD  4074  dfepfr  5647  epfrc  5648  fndmdifcom  7040  fniniseg2  7059  uniordint  7801  naddov3  8668  dfoi  9474  kmlem3  10137  alephsuc3  10566  hashbclem  14491  gcdcom  16572  gcdass  16606  lcmcom  16652  lcmass  16673  acsfn0  17717  dfinito2  18061  dftermo2  18062  dfrhm2  20557  lbsextg  21267  dmtopon  23061  fctop2  23143  ordtrest2  23342  qtopres  23836  tsmsfbas  24266  shftmbl  25678  ppiub  27349  rpvmasum  27671  noextendlt  27814  nosepne  27825  nosepdm  27829  nosupbnd2lem1  27860  noinfbnd2lem1  27875  noetasuplem4  27881  umgrislfupgrlem  29453  finsumvtxdg2ssteplem1  29876  clwwlknclwwlkdifnum  30312  clwwlknon2num  30437  dlwwlknondlwlknonf1o  30697  numclwlk1lem1  30701  3unrab  32830  aciunf1  32989  fpwrelmapffslem  33058  constrcbvlem  34126  ordtrest2NEW  34294  unelldsys  34529  rossros  34551  aean  34615  orvcval2  34830  subfacp1lem6  35658  satfv1  35836  itg2addnclem2  38304  scottexf  38798  scott0f  38799  refsymrels2  39279  dfeqvrels2  39302  refrelsredund3  39348  dffunsALTV5  39402  glbconxN  40133  primrootsunit1  42845  primrootsunit  42846  3anrabdioph  43496  3orrabdioph  43497  rexrabdioph  43504  2rexfrabdioph  43506  3rexfrabdioph  43507  4rexfrabdioph  43508  6rexfrabdioph  43509  7rexfrabdioph  43510  elnn0rabdioph  43513  elnnrabdioph  43517  rabren3dioph  43525  rmydioph  43724  rmxdioph  43726  expdiophlem2  43732  onuniintrab  43936  relintab  44292  sqrtcvallem1  44340  uzmptshftfval  45039  binomcxplemdvsum  45048  binomcxp  45050  dvnprod  46646  fourierdlem113  46916  ovnsubadd  47269  hoidmv1lelem3  47290  hoidmvlelem3  47294  ovolval3  47344  ovolval4lem2  47347  ovolval5lem3  47351  smflimlem4  47471