Theorem rabbii 3419

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

Syntax hints:   ↔ wb 207   = wceq 1522   ∈ wcel 2081  {crab 3109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-rab 3114

This theorem is referenced by:  dfdif3  4012  elneldisj  4262  elnelun  4263  dfepfr  5428  epfrc  5429  fndmdifcom  6678  fniniseg2  6697  uniordint  7377  dfoi  8821  kmlem3  9424  alephsuc3  9848  hashbclem  13658  gcdcom  15695  gcdass  15724  lcmcom  15766  lcmass  15787  acsfn0  16760  dfrhm2  19159  lbsextg  19624  dmtopon  21215  fctop2  21297  ordtrest2  21496  qtopres  21990  tsmsfbas  22419  shftmbl  23822  ppiub  25462  rpvmasum  25784  umgrislfupgrlem  26590  finsumvtxdg2ssteplem1  27010  clwwlknclwwlkdifnum  27445  clwwlknon2num  27571  dlwwlknondlwlknonf1o  27836  numclwlk1lem1  27840  aciunf1  30098  fpwrelmapffslem  30156  ordtrest2NEW  30783  unelldsys  31034  rossros  31056  aean  31120  orvcval2  31333  subfacp1lem6  32040  satfv1  32218  noextendlt  32785  nosepne  32794  nosepdm  32797  nosupbnd2lem1  32824  noetalem3  32828  itg2addnclem2  34475  scottexf  34978  scott0f  34979  rabbieq  35044  refsymrels2  35332  dfeqvrels2  35354  refrelsredund3  35400  dffunsALTV5  35451  glbconxN  36045  3anrabdioph  38864  3orrabdioph  38865  rexrabdioph  38876  2rexfrabdioph  38878  3rexfrabdioph  38879  4rexfrabdioph  38880  6rexfrabdioph  38881  7rexfrabdioph  38882  elnn0rabdioph  38885  elnnrabdioph  38889  rabren3dioph  38897  rmydioph  39096  rmxdioph  39098  expdiophlem2  39104  relintab  39428  uzmptshftfval  40216  binomcxplemdvsum  40225  binomcxp  40227  dvnprod  41775  ovnsubadd  42396  hoidmv1lelem3  42417  hoidmvlelem3  42421  ovolval3  42471  ovolval4lem2  42474  ovolval5lem3  42478  smflimlem4  42592