Theorem elequ2 2169

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 2167	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2167	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1719	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541  ax-14 2167

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2172  dveel2  2174  axext3  2176  axext4  2177  bm1.1  2178  eleq2w  2255  bm1.3ii  4151  nalset  4160  zfun  4466  fv3  5578  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  acfun  7269  ccfunen  7326  cc1  7327  nninfinf  10517  bdsepnft  15449  bdsepnfALT  15451  bdbm1.3ii  15453  bj-nalset  15457  bj-nnelirr  15515  nninfalllem1  15568  nninfsellemeq  15574  nninfsellemqall  15575  nninfsellemeqinf  15576  nninfomni  15579