Theorem isseti 3487

Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.)

Hypothesis

Ref	Expression
isseti.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
isseti	⊢ ∃𝑥 𝑥 = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem isseti

Step	Hyp	Ref	Expression
1		isseti.1	. 2 ⊢ 𝐴 ∈ V
2		elissetv 2810	. 2 ⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1534  ∃wex 1774   ∈ wcel 2099  Vcvv 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-clel 2806

This theorem is referenced by:  rexcom4b  3501  ceqsal  3507  ceqsalv  3509  ceqsexOLD  3522  ceqsexvOLD  3524  vtocl  3543  vtoclef  3548  vtoclfOLD  3550  euind  3719  eusv2nf  5395  zfpair  5421  axprALT  5422  opabn0  5555  isarep2  6644  dfoprab2  7478  rnoprab  7524  ov3  7584  omeu  8606  cflem  10270  genpass  11033  supaddc  12212  supadd  12213  supmul1  12214  supmullem2  12216  supmul  12217  ruclem13  16219  joindm  18367  meetdm  18381  dmscut  27757  bnj986  34586  satfdm  34979  fmla0  34992  fmlasuc0  34994  bj-snsetex  36442  bj-restn0  36569  bj-restuni  36576  ac6s6f  37646  tfsconcatlem  42765  elintima  43083  natlocalincr  46262  tworepnotupword  46272  funressnfv  46425  elpglem2  48143

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »