Theorem cnvexg 7890

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 6079	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6241	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5647	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7868	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2857	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5860	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7867	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2857	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7719	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5269	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 595	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2132  Vcvv 3444   ⊆ wss 3895   × cxp 5634  ^◡ccnv 5635  dom cdm 5636  ran crn 5637  Rel wrel 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-xp 5642  df-rel 5643  df-cnv 5644  df-dm 5646  df-rn 5647

This theorem is referenced by:  cnvex  7891  relcnvexb  7892  cofunex2g  7916  tposexg  8204  cnven  8999  cnvct  9000  fopwdom  9042  domssex2  9094  domssex  9095  cnvfiALT  9268  mapfienlem2  9338  wemapwe  9638  hasheqf1oi  14350  brtrclfvcnv  15003  brcnvtrclfvcnv  15004  relexpcnv  15034  relexpnnrn  15044  relexpaddg  15052  imasle  17525  cnvps  18582  gsumvalx  18682  symginv  19414  tposmap  22486  metustel  24579  metustss  24580  metustfbas  24586  metuel2  24594  psmetutop  24596  restmetu  24599  itg2gt0  25791  oldfib  28436  nlfnval  32019  fnpreimac  32811  ffsrn  32869  pwrssmgc  33128  tocycfv  33239  elrspunidl  33560  ply1degltdimlem  33863  algextdeglem8  33965  rhmpreimacnlem  34125  eulerpartlemgs2  34621  orvcval  34699  coinfliprv  34724  cossex  38946  cosscnvex  38947  cnvelrels  39013  lkrval  39650  aks6d1c2lem4  42682  aks6d1c6lem2  42726  aks6d1c6lem3  42727  pw2f1o2val  43554  lmhmlnmsplit  43602  cnvcnvintabd  44114  clrellem  44136  relexpaddss  44232  cnvtrclfv  44238  rntrclfvRP  44245  xpexb  44967  sge0f1o  46894  smfco  47314  preimafvelsetpreimafv  47932  fundcmpsurinjlem2  47943  grimcnv  48448  grlicsym  48573  imasubclem1  49663