Theorem cnvexg 7917

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 6106	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6270	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5672	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7895	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2868	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5885	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7894	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2868	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7746	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5290	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 598	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905   × cxp 5659  ^◡ccnv 5660  dom cdm 5661  ran crn 5662  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  cnvex  7918  relcnvexb  7919  cofunex2g  7943  tposexg  8232  cnven  9026  cnvct  9027  fopwdom  9069  domssex2  9121  domssex  9122  cnvfiALT  9292  mapfienlem2  9362  wemapwe  9662  hasheqf1oi  14383  brtrclfvcnv  15037  brcnvtrclfvcnv  15038  relexpcnv  15068  relexpnnrn  15078  relexpaddg  15086  imasle  17572  cnvps  18629  gsumvalx  18729  symginv  19467  tposmap  22614  metustel  24707  metustss  24708  metustfbas  24714  metuel2  24722  psmetutop  24724  restmetu  24727  itg2gt0  25919  oldfib  28570  nlfnval  32233  fnpreimac  33015  ffsrn  33073  pwrssmgc  33320  tocycfv  33429  elrspunidl  33736  ply1degltdimlem  34012  algextdeglem8  34114  rhmpreimacnlem  34274  eulerpartlemgs2  34770  orvcval  34848  coinfliprv  34873  cossex  39158  cosscnvex  39159  cnvelrels  39225  lkrval  39862  aks6d1c2lem4  42894  aks6d1c6lem2  42938  aks6d1c6lem3  42939  pw2f1o2val  43766  lmhmlnmsplit  43814  cnvcnvintabd  44326  clrellem  44348  relexpaddss  44444  cnvtrclfv  44450  rntrclfvRP  44457  xpexb  45162  sge0f1o  47096  smfco  47516  preimafvelsetpreimafv  48137  fundcmpsurinjlem2  48148  grimcnv  48653  grlicsym  48778  imasubclem1  49882