Theorem cnvexg 7876

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 6071	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6235	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5643	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7854	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2842	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5852	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7853	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2842	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7706	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5270	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   × cxp 5630  ^◡ccnv 5631  dom cdm 5632  ran crn 5633  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  cnvex  7877  relcnvexb  7878  cofunex2g  7904  tposexg  8192  cnven  8982  cnvct  8983  fopwdom  9025  domssex2  9077  domssex  9078  cnvfiALT  9251  mapfienlem2  9321  wemapwe  9618  hasheqf1oi  14286  brtrclfvcnv  14939  brcnvtrclfvcnv  14940  relexpcnv  14970  relexpnnrn  14980  relexpaddg  14988  imasle  17456  cnvps  18513  gsumvalx  18613  symginv  19343  tposmap  22413  metustel  24506  metustss  24507  metustfbas  24513  metuel2  24521  psmetutop  24523  restmetu  24526  itg2gt0  25729  oldfib  28385  nlfnval  31969  fnpreimac  32760  ffsrn  32818  pwrssmgc  33093  tocycfv  33203  elrspunidl  33521  ply1degltdimlem  33800  algextdeglem8  33902  rhmpreimacnlem  34062  eulerpartlemgs2  34558  orvcval  34636  coinfliprv  34661  cossex  38760  cosscnvex  38761  cnvelrels  38827  lkrval  39464  aks6d1c2lem4  42497  aks6d1c6lem2  42541  aks6d1c6lem3  42542  pw2f1o2val  43396  lmhmlnmsplit  43444  cnvcnvintabd  43956  clrellem  43978  relexpaddss  44074  cnvtrclfv  44080  rntrclfvRP  44087  xpexb  44809  sge0f1o  46740  smfco  47160  preimafvelsetpreimafv  47748  fundcmpsurinjlem2  47759  grimcnv  48248  grlicsym  48373  imasubclem1  49463