![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elequ1 | Structured version Visualization version GIF version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.) |
Ref | Expression |
---|---|
elequ1 | ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax8 2085 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | |
2 | ax8 2085 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) | |
3 | 2 | equcoms 2002 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) |
4 | 1, 3 | impbid 213 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 |
This theorem is referenced by: elsb3 2087 cleljust 2088 ax12wdemo 2104 cleljustALT 2337 cleljustALT2 2338 dveel1 2439 axc14 2441 axsepgfromrep 5086 nalset 5102 zfpow 5151 zfun 7311 tz7.48lem 7919 unxpdomlem1 8558 pssnn 8572 zfinf 8937 aceq1 9378 aceq0 9379 aceq2 9380 dfac3 9382 dfac5lem2 9385 dfac5lem3 9386 dfac2a 9390 kmlem4 9414 zfac 9717 nd1 9844 axextnd 9848 axrepndlem1 9849 axrepndlem2 9850 axunndlem1 9852 axunnd 9853 axpowndlem2 9855 axpowndlem3 9856 axpowndlem4 9857 axregndlem1 9859 axregnd 9861 zfcndun 9872 zfcndpow 9873 zfcndinf 9875 zfcndac 9876 fpwwe2lem12 9898 axgroth3 10088 axgroth4 10089 nqereu 10186 mdetunilem9 20901 madugsum 20924 neiptopnei 21412 2ndc1stc 21731 nrmr0reg 22029 alexsubALTlem4 22330 xrsmopn 23091 itg2cn 24035 itgcn 24114 sqff1o 25429 dya2iocuni 31114 bnj849 31769 erdsze 32013 untsucf 32489 untangtr 32493 dfon2lem3 32583 dfon2lem6 32586 dfon2lem7 32587 dfon2 32590 axextdist 32598 distel 32602 neibastop2lem 33262 bj-elequ12 33555 bj-nfeel2 33692 bj-ru0 33770 prtlem5 35477 prtlem13 35485 prtlem16 35486 ax12el 35559 pw2f1ocnv 39070 aomclem8 39097 grumnud 40071 lcosslsp 43927 |
Copyright terms: Public domain | W3C validator |