Theorem cnvexg 7680

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 5952	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6112	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5547	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7660	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2836	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5749	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7659	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2836	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7514	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5201	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 590	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853   × cxp 5534  ^◡ccnv 5535  dom cdm 5536  ran crn 5537  Rel wrel 5541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-xp 5542  df-rel 5543  df-cnv 5544  df-dm 5546  df-rn 5547

This theorem is referenced by:  cnvex  7681  relcnvexb  7682  cofunex2g  7701  tposexg  7960  cnven  8688  cnvct  8689  fopwdom  8731  domssex2  8784  domssex  8785  cnvfiALT  8936  mapfienlem2  9000  wemapwe  9290  hasheqf1oi  13883  brtrclfvcnv  14532  brcnvtrclfvcnv  14533  relexpcnv  14563  relexpnnrn  14573  relexpaddg  14581  imasle  16982  cnvps  18038  gsumvalx  18102  symginv  18748  tposmap  21308  metustel  23402  metustss  23403  metustfbas  23409  metuel2  23417  psmetutop  23419  restmetu  23422  itg2gt0  24612  nlfnval  29916  fnpreimac  30682  ffsrn  30738  pwrssmgc  30951  tocycfv  31049  elrspunidl  31274  rhmpreimacnlem  31502  eulerpartlemgs2  32013  orvcval  32090  coinfliprv  32115  cossex  36228  cosscnvex  36229  cnvelrels  36299  lkrval  36788  pw2f1o2val  40505  lmhmlnmsplit  40556  cnvcnvintabd  40825  clrellem  40847  relexpaddss  40944  cnvtrclfv  40950  rntrclfvRP  40957  xpexb  41686  sge0f1o  43538  smfco  43951  preimafvelsetpreimafv  44456  fundcmpsurinjlem2  44467