Theorem inv1 4361

Description: The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)

Assertion

Ref	Expression
inv1	⊢ (𝐴 ∩ V) = 𝐴

Proof of Theorem inv1

Step	Hyp	Ref	Expression
1		inss1 4200	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3969	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3971	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4203	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3963	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1540  Vcvv 3447   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  undif1  4439  dfif4  4504  rint0  4952  iinrab2  5034  riin0  5046  xpriindi  5800  xpssres  5989  resdmdfsn  6002  elrid  6017  imainrect  6154  xpima  6155  cnvrescnv  6168  dmresv  6173  curry1  8083  curry2  8086  fpar  8095  oev2  8487  hashresfn  14305  dmhashres  14306  gsumxp  19906  pjpm  21617  ptbasfi  23468  mbfmcst  34250  0rrv  34442  vonf1owev  35095  pol0N  39903