Theorem elequ2 2183

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 2181	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2181	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1732	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554  ax-14 2181

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2186  dveel2  2188  axext3  2190  axext4  2191  bm1.1  2192  eleq2w  2269  bm1.3ii  4181  nalset  4190  zfun  4499  fv3  5622  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  acfun  7350  ccfunen  7411  cc1  7412  nninfinf  10625  bdsepnft  16022  bdsepnfALT  16024  bdbm1.3ii  16026  bj-nalset  16030  bj-nnelirr  16088  nninfalllem1  16147  nninfsellemeq  16153  nninfsellemqall  16154  nninfsellemeqinf  16155  nninfomni  16158