Theorem elequ2 2207

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 2205	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2205	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1756	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579  ax-14 2205

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2210  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  eleq2w  2293  bm1.3ii  4215  nalset  4224  zfun  4537  fv3  5671  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  sspw1or2  7446  acfun  7465  ccfunen  7526  cc1  7527  nninfinf  10751  bdsepnft  16586  bdsepnfALT  16588  bdbm1.3ii  16590  bj-nalset  16594  bj-nnelirr  16652  nninfalllem1  16717  nninfsellemeq  16723  nninfsellemqall  16724  nninfsellemeqinf  16725  nninfomni  16728