Theorem elequ2 2153

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 2151	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2151	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1708	. 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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530  ax-14 2151

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2156  dveel2  2158  axext3  2160  axext4  2161  bm1.1  2162  eleq2w  2239  bm1.3ii  4126  nalset  4135  zfun  4436  fv3  5540  tfrlemisucaccv  6329  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  acfun  7209  ccfunen  7266  cc1  7267  bdsepnft  14827  bdsepnfALT  14829  bdbm1.3ii  14831  bj-nalset  14835  bj-nnelirr  14893  nninfalllem1  14946  nninfsellemeq  14952  nninfsellemqall  14953  nninfsellemeqinf  14954  nninfomni  14957