Theorem inteq 4910

Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.)

Assertion

Ref	Expression
inteq	⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

Proof of Theorem inteq

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raleq 3317	. . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦))
2	1	abbidv 2827	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦})
3		dfint2 4909	. 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
4		dfint2 4909	. 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2739  ∀wral 3077  ∩ cint 4907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rex 3088  df-int 4908

This theorem is used by:  inteqi  4911  inteqd  4912  unissint  4932  uniintsn  4945  rint0  4948  intex  5305  intnex  5306  elreldm  5917  elxp5  7924  1stval2  8007  oev2  8515  fundmen  9043  xpsnen  9064  fiint  9302  elfir  9391  inelfi  9394  fiin  9398  cardmin2  10061  isfin2-2  10378  incexclem  15985  mreintcl  17745  ismred2  17753  fiinopn  23199  cmpfii  23707  ptbasfi  23880  fbssint  24137  shintcl  31914  chintcl  31916  zarcmplem  34495  inelpisys  34769  rankeq1o  36902  bj-0int  37990  bj-ismoored  37996  bj-snmoore  38002  bj-prmoore  38004  neificl  38655  heibor1lem  38711  elrfi  43658  elrfirn  43659