Theorem cnvexg 7868

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 6063	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6227	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5635	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7846	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2842	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5844	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7845	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2842	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7698	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5260	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625  Rel wrel 5629

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 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  cnvex  7869  relcnvexb  7870  cofunex2g  7896  tposexg  8183  cnven  8973  cnvct  8974  fopwdom  9016  domssex2  9068  domssex  9069  cnvfiALT  9242  mapfienlem2  9312  wemapwe  9609  hasheqf1oi  14304  brtrclfvcnv  14957  brcnvtrclfvcnv  14958  relexpcnv  14988  relexpnnrn  14998  relexpaddg  15006  imasle  17478  cnvps  18535  gsumvalx  18635  symginv  19368  tposmap  22432  metustel  24525  metustss  24526  metustfbas  24532  metuel2  24540  psmetutop  24542  restmetu  24545  itg2gt0  25737  oldfib  28383  nlfnval  31967  fnpreimac  32758  ffsrn  32816  pwrssmgc  33075  tocycfv  33185  elrspunidl  33503  ply1degltdimlem  33782  algextdeglem8  33884  rhmpreimacnlem  34044  eulerpartlemgs2  34540  orvcval  34618  coinfliprv  34643  cossex  38844  cosscnvex  38845  cnvelrels  38911  lkrval  39548  aks6d1c2lem4  42580  aks6d1c6lem2  42624  aks6d1c6lem3  42625  pw2f1o2val  43485  lmhmlnmsplit  43533  cnvcnvintabd  44045  clrellem  44067  relexpaddss  44163  cnvtrclfv  44169  rntrclfvRP  44176  xpexb  44898  sge0f1o  46828  smfco  47248  preimafvelsetpreimafv  47860  fundcmpsurinjlem2  47871  grimcnv  48376  grlicsym  48501  imasubclem1  49591