Theorem eqabri 2871

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)

Hypothesis

Ref	Expression
eqabri.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
eqabri	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem eqabri

Step	Hyp	Ref	Expression
1		eqabri.1	. . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
3	2	eqabrd 2870	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1547	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109  {cab 2707

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqabcri  2872  rabid  3418  csbcow  3868  csbco  3869  csbgfi  3873  csbnestgfw  4375  csbnestgf  4380  relopabi  5769  cnv0  6093  funcnv3  6556  opabiota  6909  zfrep6  7897  frrlem2  8227  frrlem3  8228  frrlem4  8229  frrlem8  8233  fprresex  8250  tfrlem4  8308  tfrlem8  8313  tfrlem9  8314  ixpn0  8864  sbthlem1  9011  dffi3  9340  1idpr  10942  ltexprlem1  10949  ltexprlem2  10950  ltexprlem3  10951  ltexprlem4  10952  ltexprlem6  10954  ltexprlem7  10955  reclem2pr  10961  reclem3pr  10962  reclem4pr  10963  supsrlem  11024  dissnref  23431  dissnlocfin  23432  txbas  23470  xkoccn  23522  xkoptsub  23557  xkoco1cn  23560  xkoco2cn  23561  xkoinjcn  23590  mbfi1fseqlem4  25635  avril1  30425  rnmposs  32631  bnj1436  34808  bnj916  34902  bnj983  34920  bnj1083  34947  bnj1245  34983  bnj1311  34993  bnj1371  34998  bnj1398  35003  tz9.1regs  35069  setinds  35754  bj-elsngl  36944  bj-projun  36970  bj-projval  36972  f1omptsnlem  37312  icoreresf  37328  finxp0  37367  finxp1o  37368  finxpsuclem  37373  sdclem1  37725  csbcom2fi  38110  rr-grothshortbi  44279  modelaxreplem3  44957  upwordisword  46866  tworepnotupword  46871