Theorem eqneltrd 2720

Description: If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
eqneltrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqneltrd.2	⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqneltrd	⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Proof of Theorem eqneltrd

Step	Hyp	Ref	Expression
1		eqneltrd.2	. 2 ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)
2		eqneltrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	eleq1d 2686	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mtbird 315	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eqneltrrd  2721  opabn1stprc  7228  omopth2  7664  fpwwe2  9465  znnn0nn  11489  sqrtneglem  14007  dvdsaddre2b  15029  mreexmrid  16303  mplcoe1  19465  mplcoe5  19468  2sqn0  29646  reprpmtf1o  30704  fvnobday  31829  bj-snmoore  33068  islln2a  34803  islpln2a  34834  islvol2aN  34878  oddfl  39489  sumnnodd  39862  sinaover2ne0  40079  dvnprodlem1  40161  dirker2re  40309  dirkerdenne0  40310  dirkertrigeqlem3  40317  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fouriersw  40448