Theorem inteq 4973

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

Syntax hints:   → wi 4   = wceq 1537  {cab 2717  ∀wral 3067  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ral 3068  df-rex 3077  df-int 4971

This theorem is referenced by:  inteqi  4974  inteqd  4975  unissint  4996  uniintsn  5009  rint0  5012  intex  5362  intnex  5363  elreldm  5960  elxp5  7963  1stval2  8047  oev2  8579  fundmen  9096  xpsnen  9121  fiint  9394  fiintOLD  9395  elfir  9484  inelfi  9487  fiin  9491  cardmin2  10068  isfin2-2  10388  incexclem  15884  mreintcl  17653  ismred2  17661  fiinopn  22928  cmpfii  23438  ptbasfi  23610  fbssint  23867  shintcl  31362  chintcl  31364  zarcmplem  33827  inelpisys  34118  rankeq1o  36135  bj-0int  37067  bj-ismoored  37073  bj-snmoore  37079  bj-prmoore  37081  neificl  37713  heibor1lem  37769  elrfi  42650  elrfirn  42651