Theorem inpreima 7049

Description: Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)

Assertion

Ref	Expression
inpreima	⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))

Proof of Theorem inpreima

Step	Hyp	Ref	Expression
1		funcnvcnv 6592	. 2 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
2		imain 6610	. 2 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))
3	1, 2	syl 18	1 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))

Syntax hints:   → wi 4   = wceq 1563   ∩ cin 3906  ^◡ccnv 5651   “ cima 5655  Fun wfun 6519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-fun 6527

This theorem is referenced by:  cnvimainrn  7052  sspreima  7053  fimacnvinrn  7056  fsuppeq  8159  fsuppeqg  8160  ofco2  22569  cnrest2  23404  cnhaus  23472  kgencn3  23676  qtoptop2  23817  basqtop  23829  ismbfd  25759  mbfimaopn2  25777  i1fima  25798  i1fima2  25799  i1fd  25801  disjpreima  32839  smfco  47374  predisj  49440