Theorem cnvexg 7921

Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)

Assertion

Ref	Expression
cnvexg	⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Proof of Theorem cnvexg

Step	Hyp	Ref	Expression
1		relcnv 6100	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6266	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5666	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7899	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2865	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5879	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7898	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2865	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7750	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5284	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899   × cxp 5653  ^◡ccnv 5654  dom cdm 5655  ran crn 5656  Rel wrel 5660

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-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  cnvex  7922  relcnvexb  7923  cofunex2g  7947  tposexg  8238  cnven  9040  cnvct  9041  fopwdom  9083  domssex2  9135  domssex  9136  cnvfiALT  9306  mapfienlem2  9376  wemapwe  9676  hasheqf1oi  14415  brtrclfvcnv  15077  brcnvtrclfvcnv  15078  relexpcnv  15108  relexpnnrn  15118  relexpaddg  15126  imasle  17609  cnvps  18666  gsumvalx  18778  symginv  19529  tposmap  22679  metustel  24776  metustss  24777  metustfbas  24783  metuel2  24791  psmetutop  24793  restmetu  24796  itg2gt0  25988  oldfib  28642  nlfnval  32362  fnpreimac  33143  pwrssmgc  33440  tocycfv  33549  elrspunidl  33856  ply1degltdimlem  34132  algextdeglem8  34234  rhmpreimacnlem  34394  eulerpartlemgs2  34891  orvcval  34969  coinfliprv  34994  cossex  39257  cosscnvex  39258  cnvelrels  39324  lkrval  39961  aks6d1c2lem4  42993  aks6d1c6lem2  43037  aks6d1c6lem3  43038  pw2f1o2val  43880  lmhmlnmsplit  43928  cnvcnvintabd  44440  clrellem  44462  relexpaddss  44558  cnvtrclfv  44564  rntrclfvRP  44571  xpexb  45276  sge0f1o  47210  smfco  47630  preimafvelsetpreimafv  48288  fundcmpsurinjlem2  48299  grimcnv  48804  grlicsym  48929  imasubclem1  50030