Theorem elequ2 2172

Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elequ2	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax-14 2170	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2170	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1722	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 129	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544  ax-14 2170

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2175  dveel2  2177  axext3  2179  axext4  2180  bm1.1  2181  eleq2w  2258  bm1.3ii  4155  nalset  4164  zfun  4470  fv3  5584  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  acfun  7292  ccfunen  7349  cc1  7350  nninfinf  10554  bdsepnft  15641  bdsepnfALT  15643  bdbm1.3ii  15645  bj-nalset  15649  bj-nnelirr  15707  nninfalllem1  15763  nninfsellemeq  15769  nninfsellemqall  15770  nninfsellemeqinf  15771  nninfomni  15774