Theorem inteq 4909

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 3316	. . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦))
2	1	abbidv 2826	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦})
3		dfint2 4908	. 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
4		dfint2 4908	. 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cab 2738  ∀wral 3076  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rex 3087  df-int 4907

This theorem is used by:  inteqi  4910  inteqd  4911  unissint  4931  uniintsn  4944  rint0  4947  intex  5304  intnex  5305  elreldm  5916  elxp5  7935  1stval2  8018  oev2  8534  fundmen  9062  xpsnen  9083  fiint  9321  elfir  9410  inelfi  9413  fiin  9417  cardmin2  10083  isfin2-2  10400  incexclem  16010  mreintcl  17770  ismred2  17778  fiinopn  23224  cmpfii  23732  ptbasfi  23905  fbssint  24162  shintcl  31937  chintcl  31939  zarcmplem  34559  inelpisys  34833  rankeq1o  37024  bj-0int  38114  bj-ismoored  38120  bj-snmoore  38126  bj-prmoore  38128  neificl  38780  heibor1lem  38836  elrfi  43798  elrfirn  43799