Theorem elequ2 2146

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 2144	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2144	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1701	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 128	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523  ax-14 2144

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb2  2149  dveel2  2151  axext3  2153  axext4  2154  bm1.1  2155  eleq2w  2232  bm1.3ii  4110  nalset  4119  zfun  4419  fv3  5519  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  acfun  7184  ccfunen  7226  cc1  7227  bdsepnft  13922  bdsepnfALT  13924  bdbm1.3ii  13926  bj-nalset  13930  bj-nnelirr  13988  nninfalllem1  14041  nninfsellemeq  14047  nninfsellemqall  14048  nninfsellemeqinf  14049  nninfomni  14052