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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-rab 3416

This theorem is referenced by:  rabbieq  3424  dfdif3OLD  4093  elneldisj  4367  elnelun  4368  dfepfr  5638  epfrc  5639  fndmdifcom  7033  fniniseg2  7052  uniordint  7795  naddov3  8692  dfoi  9525  kmlem3  10167  alephsuc3  10594  hashbclem  14470  gcdcom  16532  gcdass  16566  lcmcom  16612  lcmass  16633  acsfn0  17672  dfinito2  18016  dftermo2  18017  dfrhm2  20434  lbsextg  21123  dmtopon  22861  fctop2  22943  ordtrest2  23142  qtopres  23636  tsmsfbas  24066  shftmbl  25491  ppiub  27167  rpvmasum  27489  noextendlt  27633  nosepne  27644  nosepdm  27648  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  umgrislfupgrlem  29101  finsumvtxdg2ssteplem1  29525  clwwlknclwwlkdifnum  29961  clwwlknon2num  30086  dlwwlknondlwlknonf1o  30346  numclwlk1lem1  30350  3unrab  32484  aciunf1  32641  fpwrelmapffslem  32709  constrcbvlem  33789  ordtrest2NEW  33954  unelldsys  34189  rossros  34211  aean  34275  orvcval2  34491  subfacp1lem6  35207  satfv1  35385  itg2addnclem2  37696  scottexf  38192  scott0f  38193  refsymrels2  38583  dfeqvrels2  38606  refrelsredund3  38652  dffunsALTV5  38705  glbconxN  39397  primrootsunit1  42110  primrootsunit  42111  3anrabdioph  42805  3orrabdioph  42806  rexrabdioph  42817  2rexfrabdioph  42819  3rexfrabdioph  42820  4rexfrabdioph  42821  6rexfrabdioph  42822  7rexfrabdioph  42823  elnn0rabdioph  42826  elnnrabdioph  42830  rabren3dioph  42838  rmydioph  43038  rmxdioph  43040  expdiophlem2  43046  onuniintrab  43250  relintab  43607  sqrtcvallem1  43655  uzmptshftfval  44370  binomcxplemdvsum  44379  binomcxp  44381  dvnprod  45978  ovnsubadd  46601  hoidmv1lelem3  46622  hoidmvlelem3  46626  ovolval3  46676  ovolval4lem2  46679  ovolval5lem3  46683  smflimlem4  46803