Theorem cnvexg 7937

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 6099	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6271	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5661	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7915	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2865	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5876	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7914	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2865	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7766	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5280	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   × cxp 5648  ^◡ccnv 5649  dom cdm 5650  ran crn 5651  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  cnvex  7938  relcnvexb  7939  cofunex2g  7963  tposexg  8261  cnven  9065  cnvct  9066  fopwdom  9108  domssex2  9160  domssex  9161  cnvfiALT  9332  mapfienlem2  9402  wemapwe  9702  hasheqf1oi  14499  brtrclfvcnv  15163  brcnvtrclfvcnv  15164  relexpcnv  15194  relexpnnrn  15204  relexpaddg  15212  imasle  17701  cnvps  18758  gsumvalx  18871  symginv  19622  tposmap  22778  metustel  24875  metustss  24876  metustfbas  24882  metuel2  24890  psmetutop  24892  restmetu  24895  itg2gt0  26087  oldfib  28769  nlfnval  32489  fnpreimac  33312  pwrssmgc  33608  tocycfv  33717  ply1degltdimlem  34301  algextdeglem8  34403  rhmpreimacnlem  34563  eulerpartlemgs2  35059  orvcval  35137  coinfliprv  35162  cossex  39535  cosscnvex  39536  cnvelrels  39602  lkrval  40239  aks6d1c2lem4  43271  aks6d1c6lem2  43315  aks6d1c6lem3  43316  pw2f1o2val  44140  lmhmlnmsplit  44183  cnvcnvintabd  44694  clrellem  44716  relexpaddss  44812  cnvtrclfv  44818  rntrclfvRP  44825  xpexb  45530  sge0f1o  47486  smfco  47906  preimafvelsetpreimafv  48564  fundcmpsurinjlem2  48575  grimcnv  49080  grlicsym  49205  imasubclem1  50314