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 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  rabbieq  3420  dfepfr  5634  epfrc  5635  fndmdifcom  7043  fniniseg2  7062  uniordint  7816  naddov3  8694  dfoi  9509  kmlem3  10235  alephsuc3  10669  hashbclem  14601  gcdcom  16691  gcdass  16726  lcmcom  16774  lcmass  16795  acsfn0  17840  dfinito2  18184  dftermo2  18185  dfrhm2  20710  lbsextg  21446  dmtopon  23247  fctop2  23329  ordtrest2  23528  qtopres  24023  tsmsfbas  24453  shftmbl  25865  ppiub  27537  rpvmasum  27859  noextendlt  28032  nosepne  28043  nosepdm  28047  nosupbnd2lem1  28078  noinfbnd2lem1  28093  noetasuplem4  28099  umgrislfupgrlem  29706  finsumvtxdg2ssteplem1  30132  clwwlknclwwlkdifnum  30577  clwwlknon2num  30702  dlwwlknondlwlknonf1o  30972  numclwlk1lem1  30976  3unrab  33147  aciunf1  33305  fpwrelmapffslem  33371  constrcbvlem  34434  ordtrest2NEW  34602  unelldsys  34838  rossros  34860  aean  34924  orvcval2  35138  subfacp1lem6  36037  satfv1  36215  itg2addnclem2  38684  scottexf  39194  scott0f  39195  refsymrels2  39675  dfeqvrels2  39698  refrelsredund3  39744  dffunsALTV5  39798  glbconxN  40529  primrootsunit1  43241  primrootsunit  43242  3anrabdioph  43887  3orrabdioph  43888  rexrabdioph  43895  2rexfrabdioph  43897  3rexfrabdioph  43898  4rexfrabdioph  43899  6rexfrabdioph  43900  7rexfrabdioph  43901  elnn0rabdioph  43904  elnnrabdioph  43908  rabren3dioph  43916  rmydioph  44115  rmxdioph  44117  expdiophlem2  44123  onuniintrab  44322  relintab  44678  sqrtcvallem1  44725  uzmptshftfval  45424  binomcxplemdvsum  45433  binomcxp  45435  dvnprod  47053  fourierdlem113  47323  ovnsubadd  47676  hoidmv1lelem3  47697  hoidmvlelem3  47701  ovolval3  47751  ovolval4lem2  47754  ovolval5lem3  47758  smflimlem4  47878