Theorem abeq2i 2873

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
abeq2i.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
abeq2i	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeq2i.1	. . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
3	2	abeq2d 2872	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1546	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1539  ⊤wtru 1540   ∈ wcel 2104  {cab 2713

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814

This theorem is referenced by:  abeq1i  2874  rabid  3322  csbcow  3852  csbco  3853  csbgfi  3858  csbnestgfw  4359  csbnestgf  4364  ssrelOLD  5705  relopabi  5744  cnv0  6059  funcnv3  6533  opabiota  6883  zfrep6  7829  frrlem2  8134  frrlem3  8135  frrlem4  8136  frrlem8  8140  fprresex  8157  wfrlem2OLD  8171  wfrlem3OLD  8172  wfrlem4OLD  8174  wfrdmclOLD  8179  tfrlem4  8241  tfrlem8  8246  tfrlem9  8247  ixpn0  8749  sbthlem1  8908  dffi3  9234  1idpr  10831  ltexprlem1  10838  ltexprlem2  10839  ltexprlem3  10840  ltexprlem4  10841  ltexprlem6  10843  ltexprlem7  10844  reclem2pr  10850  reclem3pr  10851  reclem4pr  10852  supsrlem  10913  dissnref  22724  dissnlocfin  22725  txbas  22763  xkoccn  22815  xkoptsub  22850  xkoco1cn  22853  xkoco2cn  22854  xkoinjcn  22883  mbfi1fseqlem4  24928  avril1  28872  rnmposs  31056  bnj1436  32864  bnj916  32958  bnj983  32976  bnj1083  33003  bnj1245  33039  bnj1311  33049  bnj1371  33054  bnj1398  33059  setinds  33799  bj-elsngl  35202  bj-projun  35228  bj-projval  35230  f1omptsnlem  35551  icoreresf  35567  finxp0  35606  finxp1o  35607  finxpsuclem  35612  sdclem1  35945  csbcom2fi  36330  rr-grothshortbi  41959  upwordisword  46574  tworepnotupword  46579