Theorem eqabri 2879

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 2878	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1547	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810

This theorem is referenced by:  eqabcri  2880  rabid  3442  csbcow  3894  csbco  3895  csbgfi  3899  csbnestgfw  4402  csbnestgf  4407  ssrelOLD  5767  relopabi  5806  cnv0  6134  funcnv3  6611  opabiota  6966  zfrep6  7958  frrlem2  8291  frrlem3  8292  frrlem4  8293  frrlem8  8297  fprresex  8314  wfrlem2OLD  8328  wfrlem3OLD  8329  wfrlem4OLD  8331  wfrdmclOLD  8336  tfrlem4  8398  tfrlem8  8403  tfrlem9  8404  ixpn0  8949  sbthlem1  9102  dffi3  9448  1idpr  11048  ltexprlem1  11055  ltexprlem2  11056  ltexprlem3  11057  ltexprlem4  11058  ltexprlem6  11060  ltexprlem7  11061  reclem2pr  11067  reclem3pr  11068  reclem4pr  11069  supsrlem  11130  dissnref  23471  dissnlocfin  23472  txbas  23510  xkoccn  23562  xkoptsub  23597  xkoco1cn  23600  xkoco2cn  23601  xkoinjcn  23630  mbfi1fseqlem4  25676  avril1  30449  rnmposs  32657  bnj1436  34875  bnj916  34969  bnj983  34987  bnj1083  35014  bnj1245  35050  bnj1311  35060  bnj1371  35065  bnj1398  35070  setinds  35801  bj-elsngl  36991  bj-projun  37017  bj-projval  37019  f1omptsnlem  37359  icoreresf  37375  finxp0  37414  finxp1o  37415  finxpsuclem  37420  sdclem1  37772  csbcom2fi  38157  rr-grothshortbi  44294  modelaxreplem3  44972  upwordisword  46877  tworepnotupword  46882