Theorem eqabri 2904

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  eqabcri  2905  rabid  3435  csbcow  3865  csbco  3866  csbgfi  3870  csbnestgfw  4383  csbnestgf  4388  relopabi  5807  cnv0OLD  5868  funcnv3  6607  opabiota  6964  zfrep6OLD  7956  frrlem2  8290  frrlem3  8291  frrlem4  8292  frrlem8  8296  fprresex  8313  tfrlem4  8371  tfrlem8  8377  tfrlem9  8378  ixpn0  8941  sbthlem1  9089  dffi3  9405  setinds  9732  1idpr  11042  ltexprlem1  11049  ltexprlem2  11050  ltexprlem3  11051  ltexprlem4  11052  ltexprlem6  11054  ltexprlem7  11055  reclem2pr  11061  reclem3pr  11062  reclem4pr  11063  supsrlem  11124  dissnref  23760  dissnlocfin  23761  txbas  23799  xkoccn  23851  xkoptsub  23886  xkoco1cn  23889  xkoco2cn  23890  xkoinjcn  23919  mbfi1fseqlem4  25952  avril1  30951  rnmposs  33154  bnj1436  35356  bnj916  35450  bnj983  35468  bnj1083  35495  bnj1245  35531  bnj1311  35541  bnj1371  35546  bnj1398  35551  tz9.1regs  35668  bj-elsngl  37720  bj-projun  37746  bj-projval  37748  f1omptsnlem  38098  icoreresf  38114  finxp0  38153  finxp1o  38154  finxpsuclem  38159  sdclem1  38501  csbcom2fi  38884  ralrnmo  39117  raldmqsmo  39119  rr-grothshortbi  45135  modelaxreplem3  45811