Theorem cnvimass 5116

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)

Assertion

Ref	Expression
cnvimass	⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 5103	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 4939	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 3272	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3210  ^◡ccnv 4739  dom cdm 4740  ran crn 4741   “ cima 4743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4221  ax-pow 4279  ax-pr 4314

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3667  df-sn 3688  df-pr 3689  df-op 3691  df-br 4103  df-opab 4165  df-xp 4746  df-cnv 4748  df-dm 4750  df-rn 4751  df-res 4752  df-ima 4753

This theorem is referenced by:  fvimacnvi  5783  elpreima  5788  fconst4m  5895  fsuppeq  6438  fsuppeqg  6439  pw2f1odclem  7078  nn0supp  9538  fisumss  12056  fprodssdc  12254  1arith  13043  ghmpreima  13957  psrbagfi  14794  cnpnei  15054  cnclima  15058  cnntri  15059  cnntr  15060  cncnp  15065  cnrest2  15071  cndis  15076  txcnmpt  15108  txdis1cn  15113  hmeoimaf1o  15149  xmeter  15271