Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq2s | GIF version |
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
eleq2s.1 | ⊢ (𝐴 ∈ 𝐵 → 𝜑) |
eleq2s.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
eleq2s | ⊢ (𝐴 ∈ 𝐶 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2s.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
2 | 1 | eleq2i 2224 | . 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵) |
3 | eleq2s.1 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 120 | 1 ⊢ (𝐴 ∈ 𝐶 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1335 ∈ wcel 2128 |
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-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 df-clel 2153 |
This theorem is referenced by: elrabi 2865 opelopabsb 4222 epelg 4252 reg3exmidlemwe 4540 elxpi 4604 optocl 4664 fvmptss2 5545 fvmptssdm 5554 acexmidlemcase 5821 elmpocl 6020 mpoxopn0yelv 6188 tfr2a 6270 tfri1dALT 6300 2oconcl 6388 el2oss1o 6392 ecexr 6487 ectocld 6548 ecoptocl 6569 eroveu 6573 mapsnconst 6641 diffitest 6834 en2eqpr 6854 ctssdccl 7057 exmidonfinlem 7130 exmidfodomrlemr 7139 exmidfodomrlemrALT 7140 dmaddpqlem 7299 nqpi 7300 nq0nn 7364 0nsr 7671 suplocsrlempr 7729 cnm 7754 axaddcl 7786 axmulcl 7788 aprcl 8525 peano2uzs 9500 fzssnn 9976 fzossnn0 10083 rebtwn2zlemstep 10161 fldiv4p1lem1div2 10213 frecfzennn 10334 fser0const 10424 facnn 10612 bcpasc 10651 hashfzo0 10708 rexuz3 10901 rexanuz2 10902 r19.2uz 10904 cau4 11027 caubnd2 11028 climshft2 11214 climaddc1 11237 climmulc2 11239 climsubc1 11240 climsubc2 11241 climlec2 11249 climcau 11255 climcaucn 11259 iserabs 11383 binomlem 11391 isumshft 11398 cvgratgt0 11441 clim2divap 11448 ntrivcvgap 11456 fprodntrivap 11492 fprodeq0 11525 infssuzex 11848 infssuzledc 11849 3prm 12020 phicl2 12104 phibndlem 12106 dfphi2 12110 crth 12114 phimullem 12115 znnen 12197 ennnfonelemkh 12211 bj-el2oss1o 13419 2o01f 13639 nninfalllem1 13651 nninfall 13652 |
Copyright terms: Public domain | W3C validator |