![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqidd | GIF version |
Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.) |
Ref | Expression |
---|---|
eqidd | ⊢ (φ → A = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2037 | . 2 ⊢ A = A | |
2 | 1 | a1i 9 | 1 ⊢ (φ → A = A) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1242 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: cbvraldva 2533 cbvrexdva 2534 nelrdva 2740 opeq2 3541 mpteq1 3832 tfisi 4253 feq23d 4985 fvmptdv2 5203 elrnrexdm 5249 fmptco 5273 ftpg 5290 fliftfun 5379 fliftval 5383 cbvmpt2 5525 eqfnov2 5550 ovmpt2d 5570 ovmpt2dv2 5576 fnofval 5663 ofrval 5664 off 5666 ofres 5667 suppssof1 5670 ofco 5671 caofref 5674 caofrss 5677 caoftrn 5678 rdgivallem 5908 iserd 6068 fzo0to3tp 8845 iseqovex 8899 |
Copyright terms: Public domain | W3C validator |