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  7290  ccfunen  7347  cc1  7348  nninfinf  10552  bdsepnft  15617  bdsepnfALT  15619  bdbm1.3ii  15621  bj-nalset  15625  bj-nnelirr  15683  nninfalllem1  15739  nninfsellemeq  15745  nninfsellemqall  15746  nninfsellemeqinf  15747  nninfomni  15750