Theorem inv1 4362

Description: The intersection of a class with the universal class is itself. Dual of un0 4358. 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 4197	. 2 ⊢ (𝐴 ∩ V) ⊆ 𝐴
2		ssid 3967	. . 3 ⊢ 𝐴 ⊆ 𝐴
3		ssv 3969	. . 3 ⊢ 𝐴 ⊆ V
4	2, 3	ssini 4200	. 2 ⊢ 𝐴 ⊆ (𝐴 ∩ V)
5	1, 4	eqssi 3961	1 ⊢ (𝐴 ∩ V) = 𝐴

Syntax hints:   = wceq 1567  Vcvv 3463   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  vvin  4372  undif1  4442  dfif4  4508  rint0  4957  iinrab2  5038  riin0  5052  xpriindi  5823  xpssres  6018  resdmdfsn  6032  resdmdfsnOLD  6033  elrid  6049  imainrect  6180  xpima  6181  cnvrescnv  6195  dmresv  6200  imadifssran  6203  curry1  8098  curry2  8101  fpar  8110  oev2  8507  hashresfn  14375  dmhashres  14376  gsumxp  20045  pjpm  21826  ptbasfi  23706  mbfmcst  34593  0rrv  34785  fineqvomon  35453  vonf1wev  35490  vonf1owevOLD  35492  ecqmap  38987  pol0N  40572