Theorem elequ2 1692

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 1493	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 1493	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1685	. 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 1426  ax-ie2 1471  ax-8 1483  ax-14 1493  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb4  1953  dveel2  1997  axext3  2123  axext4  2124  bm1.1  2125  eleq2w  2202  bm1.3ii  4057  nalset  4066  zfun  4364  fv3  5452  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  acfun  7080  ccfunen  7096  cc1  7097  bdsepnft  13256  bdsepnfALT  13258  bdbm1.3ii  13260  bj-nalset  13264  bj-nnelirr  13322  nninfalllem1  13378  nninfsellemeq  13385  nninfsellemqall  13386  nninfsellemeqinf  13387  nninfomni  13390