Theorem cnvexg 7934

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 6100	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6270	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5662	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7912	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2866	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5877	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7911	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2866	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7763	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5281	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899   × cxp 5649  ^◡ccnv 5650  dom cdm 5651  ran crn 5652  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  cnvex  7935  relcnvexb  7936  cofunex2g  7960  tposexg  8250  cnven  9054  cnvct  9055  fopwdom  9097  domssex2  9149  domssex  9150  cnvfiALT  9321  mapfienlem2  9391  wemapwe  9691  hasheqf1oi  14488  brtrclfvcnv  15150  brcnvtrclfvcnv  15151  relexpcnv  15181  relexpnnrn  15191  relexpaddg  15199  imasle  17688  cnvps  18745  gsumvalx  18858  symginv  19609  tposmap  22765  metustel  24862  metustss  24863  metustfbas  24869  metuel2  24877  psmetutop  24879  restmetu  24882  itg2gt0  26074  oldfib  28756  nlfnval  32476  fnpreimac  33257  pwrssmgc  33554  tocycfv  33663  elrspunidl  33971  ply1degltdimlem  34247  algextdeglem8  34349  rhmpreimacnlem  34509  eulerpartlemgs2  35005  orvcval  35083  coinfliprv  35108  cossex  39421  cosscnvex  39422  cnvelrels  39488  lkrval  40125  aks6d1c2lem4  43157  aks6d1c6lem2  43201  aks6d1c6lem3  43202  pw2f1o2val  44025  lmhmlnmsplit  44073  cnvcnvintabd  44585  clrellem  44607  relexpaddss  44703  cnvtrclfv  44709  rntrclfvRP  44716  xpexb  45421  sge0f1o  47361  smfco  47781  preimafvelsetpreimafv  48439  fundcmpsurinjlem2  48450  grimcnv  48955  grlicsym  49080  imasubclem1  50181