Theorem inteq 4902

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

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  ∀wral 3044  ∩ cint 4899

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-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rex 3054  df-int 4900

This theorem is referenced by:  inteqi  4903  inteqd  4904  unissint  4925  uniintsn  4938  rint0  4941  intex  5286  intnex  5287  elreldm  5881  elxp5  7863  1stval2  7948  oev2  8448  fundmen  8963  xpsnen  8985  fiint  9235  fiintOLD  9236  elfir  9324  inelfi  9327  fiin  9331  cardmin2  9914  isfin2-2  10232  incexclem  15761  mreintcl  17515  ismred2  17523  fiinopn  22804  cmpfii  23312  ptbasfi  23484  fbssint  23741  shintcl  31292  chintcl  31294  zarcmplem  33847  inelpisys  34120  rankeq1o  36144  bj-0int  37074  bj-ismoored  37080  bj-snmoore  37086  bj-prmoore  37088  neificl  37732  heibor1lem  37788  elrfi  42667  elrfirn  42668