Theorem rabbii 3394

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390

This theorem is referenced by:  rabbieq  3397  dfdif3OLD  4058  dfepfr  5615  epfrc  5616  fndmdifcom  6995  fniniseg2  7014  uniordint  7755  naddov3  8616  dfoi  9426  kmlem3  10075  alephsuc3  10503  hashbclem  14414  gcdcom  16482  gcdass  16516  lcmcom  16562  lcmass  16583  acsfn0  17626  dfinito2  17970  dftermo2  17971  dfrhm2  20454  lbsextg  21160  dmtopon  22888  fctop2  22970  ordtrest2  23169  qtopres  23663  tsmsfbas  24093  shftmbl  25505  ppiub  27167  rpvmasum  27489  noextendlt  27633  nosepne  27644  nosepdm  27648  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  umgrislfupgrlem  29191  finsumvtxdg2ssteplem1  29614  clwwlknclwwlkdifnum  30050  clwwlknon2num  30175  dlwwlknondlwlknonf1o  30435  numclwlk1lem1  30439  3unrab  32573  aciunf1  32736  fpwrelmapffslem  32805  constrcbvlem  33899  ordtrest2NEW  34067  unelldsys  34302  rossros  34324  aean  34388  orvcval2  34603  subfacp1lem6  35367  satfv1  35545  itg2addnclem2  37993  scottexf  38489  scott0f  38490  refsymrels2  38970  dfeqvrels2  38993  refrelsredund3  39039  dffunsALTV5  39093  glbconxN  39824  primrootsunit1  42536  primrootsunit  42537  3anrabdioph  43214  3orrabdioph  43215  rexrabdioph  43222  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  elnn0rabdioph  43231  elnnrabdioph  43235  rabren3dioph  43243  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  onuniintrab  43654  relintab  44010  sqrtcvallem1  44058  uzmptshftfval  44773  binomcxplemdvsum  44782  binomcxp  44784  dvnprod  46377  ovnsubadd  47000  hoidmv1lelem3  47021  hoidmvlelem3  47025  ovolval3  47075  ovolval4lem2  47078  ovolval5lem3  47082  smflimlem4  47202