Theorem cnvexg 7964

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 6134	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6299	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5711	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7942	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2849	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5920	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7941	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2849	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7786	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5341	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 586	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  cnvex  7965  relcnvexb  7966  cofunex2g  7990  tposexg  8281  cnven  9098  cnvct  9099  fopwdom  9146  domssex2  9203  domssex  9204  cnvfiALT  9407  mapfienlem2  9475  wemapwe  9766  hasheqf1oi  14400  brtrclfvcnv  15053  brcnvtrclfvcnv  15054  relexpcnv  15084  relexpnnrn  15094  relexpaddg  15102  imasle  17583  cnvps  18648  gsumvalx  18714  symginv  19444  tposmap  22484  metustel  24584  metustss  24585  metustfbas  24591  metuel2  24599  psmetutop  24601  restmetu  24604  itg2gt0  25815  nlfnval  31913  fnpreimac  32689  ffsrn  32743  pwrssmgc  32973  tocycfv  33102  elrspunidl  33421  ply1degltdimlem  33635  algextdeglem8  33715  rhmpreimacnlem  33830  eulerpartlemgs2  34345  orvcval  34422  coinfliprv  34447  cossex  38375  cosscnvex  38376  cnvelrels  38451  lkrval  39044  aks6d1c2lem4  42084  aks6d1c6lem2  42128  aks6d1c6lem3  42129  pw2f1o2val  42996  lmhmlnmsplit  43044  cnvcnvintabd  43562  clrellem  43584  relexpaddss  43680  cnvtrclfv  43686  rntrclfvRP  43693  xpexb  44423  sge0f1o  46303  smfco  46723  preimafvelsetpreimafv  47262  fundcmpsurinjlem2  47273  grimcnv  47763  grlicsym  47830